Theorem abeqb ≪ | index | src | ≫

theorem abeqb {x: nat} (p q: wff x): $ A. x (p <-> q) <-> {x | p} == {x | q} $;

Step	Hyp	Ref	Expression
1		abeq	A. x (p <-> q) -> {x \| p} == {x \| q}
2		nfab1	FS/ x {x \| p}
3		nfab1	FS/ x {x \| q}
4	2, 3	nfeqs	F/ x {x \| p} == {x \| q}
5		bieq	(x e. {x \| p} <-> p) -> (x e. {x \| q} <-> q) -> (x e. {x \| p} <-> x e. {x \| q} <-> (p <-> q))
6		abid	x e. {x \| p} <-> p
7	5, 6	ax_mp	(x e. {x \| q} <-> q) -> (x e. {x \| p} <-> x e. {x \| q} <-> (p <-> q))
8		abid	x e. {x \| q} <-> q
9	7, 8	ax_mp	x e. {x \| p} <-> x e. {x \| q} <-> (p <-> q)
10		eleq2	{x \| p} == {x \| q} -> (x e. {x \| p} <-> x e. {x \| q})
11	9, 10	sylib	{x \| p} == {x \| q} -> (p <-> q)
12	4, 11	ialdh	{x \| p} == {x \| q} -> A. x (p <-> q)
13	1, 12	ibii	A. x (p <-> q) <-> {x \| p} == {x \| q}

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)