Theorem nfex ≪ | index | src | ≫

theorem nfex {x y: nat} (a: wff x y): $ F/ x a $ > $ F/ x E. y a $;

Step	Hyp	Ref	Expression
1		hyp h	F/ x a
2	1	nfnot	F/ x ~a
3	2	nfal	F/ x A. y ~a
4	3	nfnot	F/ x ~A. y ~a
5	4	conv ex	F/ x E. y a

Axiom use

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