Theorem nfpred

Description: Bound-variable hypothesis builder for the predecessor class. (Contributed by Scott Fenton, 9-Jun-2018)

	Ref	Expression
Hypotheses	nfpred.1	|- F/_ x R
	nfpred.2	|- F/_ x A
	nfpred.3	|- F/_ x X
Assertion	nfpred	|- F/_ x Pred ( R , A , X )

Proof

Step	Hyp	Ref	Expression
1		nfpred.1	|- F/_ x R
2		nfpred.2	|- F/_ x A
3		nfpred.3	|- F/_ x X
4		df-pred	|- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
5	1	nfcnv	|- F/_ x `' R
6	3	nfsn	|- F/_ x { X }
7	5 6	nfima	|- F/_ x ( `' R " { X } )
8	2 7	nfin	|- F/_ x ( A i^i ( `' R " { X } ) )
9	4 8	nfcxfr	|- F/_ x Pred ( R , A , X )