Theorem nfab ≪ | index | src | ≫

theorem nfab {x y: nat} (p: wff x y): $ F/ x p $ > $ FS/ x {y | p} $;

Step	Hyp	Ref	Expression
1		elab	z e. {y \| p} <-> [z / y] p
2		hyp h	F/ x p
3	2	nfsb	F/ x [z / y] p
4	1, 3	nfx	F/ x z e. {y \| p}
5	4	nfsri	FS/ x {y \| 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)