Theorem nfpred

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

	Ref	Expression
Hypotheses	nfpred.1	⊢ Ⅎ 𝑥 𝑅
	nfpred.2	⊢ Ⅎ 𝑥 𝐴
	nfpred.3	⊢ Ⅎ 𝑥 𝑋
Assertion	nfpred	⊢ Ⅎ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		nfpred.1	⊢ Ⅎ 𝑥 𝑅
2		nfpred.2	⊢ Ⅎ 𝑥 𝐴
3		nfpred.3	⊢ Ⅎ 𝑥 𝑋
4		df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
5	1	nfcnv	⊢ Ⅎ 𝑥 ◡ 𝑅
6	3	nfsn	⊢ Ⅎ 𝑥 { 𝑋 }
7	5 6	nfima	⊢ Ⅎ 𝑥 ( ◡ 𝑅 “ { 𝑋 } )
8	2 7	nfin	⊢ Ⅎ 𝑥 ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
9	4 8	nfcxfr	⊢ Ⅎ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑋 )