Theorem elab2 ≪ | index | src | ≫

theorem elab2 {x: nat} (a: nat x) (p: wff x): $ a e. {x | p} <-> [a / x] p $;

Step	Hyp	Ref	Expression
1		bitr	(a e. {x \| p} <-> [a / y] [y / x] p) -> ([a / y] [y / x] p <-> [a / x] p) -> (a e. {x \| p} <-> [a / x] p)
2		bitr	(a e. {x \| p} <-> a e. {y \| [y / x] p}) -> (a e. {y \| [y / x] p} <-> [a / y] [y / x] p) -> (a e. {x \| p} <-> [a / y] [y / x] p)
3		eleq2	{x \| p} == {y \| [y / x] p} -> (a e. {x \| p} <-> a e. {y \| [y / x] p})
4		nfv	F/ y p
5		nfsb1	F/ x [y / x] p
6		sbq	x = y -> (p <-> [y / x] p)
7	4, 5, 6	cbvabh	{x \| p} == {y \| [y / x] p}
8	3, 7	ax_mp	a e. {x \| p} <-> a e. {y \| [y / x] p}
9	2, 8	ax_mp	(a e. {y \| [y / x] p} <-> [a / y] [y / x] p) -> (a e. {x \| p} <-> [a / y] [y / x] p)
10		elab	a e. {y \| [y / x] p} <-> [a / y] [y / x] p
11	9, 10	ax_mp	a e. {x \| p} <-> [a / y] [y / x] p
12	1, 11	ax_mp	([a / y] [y / x] p <-> [a / x] p) -> (a e. {x \| p} <-> [a / x] p)
13		sbco	[a / y] [y / x] p <-> [a / x] p
14	12, 13	ax_mp	a e. {x \| p} <-> [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)