Theorem nfex1 ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		ax_10	~A. x ~a -> A. x ~A. x ~a
2	1	conv ex	E. x a -> A. x E. x a
3	2	ax_gen	A. x (E. x a -> A. x E. x a)
4	3	conv nf	F/ x E. x a

Axiom use

axs_pred_calc (ax_gen, ax_10)