Theorem nfsv ≪ | index | src | ≫

theorem nfsv (A: set) {x: nat}: $ FS/ x A $;

Step	Hyp	Ref	Expression
1		nfv	F/ x y e. A
2	1	ax_gen	A. y (F/ x y e. A)
3	2	conv nfs	FS/ x A

Axiom use

axs_pred_calc (ax_gen, ax_5)