Theorem nfnri ≪ | index | src | ≫

theorem nfnri {x y: nat} (a: nat x): $ F/ x y = a $ > $ FN/ x a $;

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