Theorem nfv ≪ | index | src | ≫

theorem nfv (a: wff) {x: nat}: $ F/ x a $;

Step	Hyp	Ref	Expression
1		ax_5	a -> A. x a
2	1	ax_gen	A. x (a -> A. x a)
3	2	conv nf	F/ x a

Axiom use

axs_pred_calc (ax_gen, ax_5)