Theorem nfsri ≪ | index | src | ≫

theorem nfsri {x y: nat} (A: set x): $ F/ x y e. A $ > $ FS/ x A $;

Step	Hyp	Ref	Expression
1		hyp h	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)