Theorem abeqv ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		bitr3	(A. x (p <-> T.) <-> {x \| p} == _V) -> (A. x (p <-> T.) <-> A. x p) -> ({x \| p} == _V <-> A. x p)
2		abeqb	A. x (p <-> T.) <-> {x \| p} == {x \| T.}
3	2	conv Univ	A. x (p <-> T.) <-> {x \| p} == _V
4	1, 3	ax_mp	(A. x (p <-> T.) <-> A. x p) -> ({x \| p} == _V <-> A. x p)
5		bibi2	T. -> (p <-> T. <-> p)
6		itru	T.
7	5, 6	ax_mp	p <-> T. <-> p
8	7	aleqi	A. x (p <-> T.) <-> A. x p
9	4, 8	ax_mp	{x \| p} == _V <-> 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)