Theorem eqab2d ≪ | index | src | ≫

theorem eqab2d (A: set) (G: wff) {x: nat} (p: wff x):
  $ G -> (x e. A <-> p) $ >
  $ G -> A == {x | p} $;

Step	Hyp	Ref	Expression
1		nfv	F/ y x e. A <-> p
2		nfv	F/ x y e. A
3		nfab1	FS/ x {x \| p}
4	3	nfel2	F/ x y e. {x \| p}
5	2, 4	nfbi	F/ x y e. A <-> y e. {x \| p}
6		eleq1	x = y -> (x e. A <-> y e. A)
7		abid	x e. {x \| p} <-> p
8		eleq1	x = y -> (x e. {x \| p} <-> y e. {x \| p})
9	7, 8	syl5bbr	x = y -> (p <-> y e. {x \| p})
10	6, 9	bieqd	x = y -> (x e. A <-> p <-> (y e. A <-> y e. {x \| p}))
11	1, 5, 10	cbvalh	A. x (x e. A <-> p) <-> A. y (y e. A <-> y e. {x \| p})
12	11	conv eqs	A. x (x e. A <-> p) <-> A == {x \| p}
13		hyp h	G -> (x e. A <-> p)
14	13	iald	G -> A. x (x e. A <-> p)
15	12, 14	sylib	G -> A == {x \| p}

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8)