Theorem nfnv ≪ | index | src | ≫

theorem nfnv (a: nat) {x: nat}: $ FN/ x a $;

Step	Hyp	Ref	Expression
1		nfv	F/ x y = a
2	1	ax_gen	A. y (F/ x y = a)
3	2	conv nfn	FN/ x a

Axiom use

axs_pred_calc (ax_gen, ax_5)