Theorem nfpred

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

	Ref	Expression
Hypotheses	nfpred.1	$$⊢\underset{\_}{Ⅎ}xR$$
	nfpred.2	$$⊢\underset{\_}{Ⅎ}xA$$
	nfpred.3	$$⊢\underset{\_}{Ⅎ}xX$$
Assertion	nfpred	$$⊢\underset{\_}{Ⅎ}xPred\left(R,A,X\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfpred.1	$$⊢\underset{\_}{Ⅎ}xR$$
2		nfpred.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		nfpred.3	$$⊢\underset{\_}{Ⅎ}xX$$
4		df-pred	$$⊢Pred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$
5	1	nfcnv	$$⊢\underset{\_}{Ⅎ}x{R}^{-1}$$
6	3	nfsn	$$⊢\underset{\_}{Ⅎ}x\left\{X\right\}$$
7	5 6	nfima	$$⊢\underset{\_}{Ⅎ}x{R}^{-1}\left[\left\{X\right\}\right]$$
8	2 7	nfin	$$⊢\underset{\_}{Ⅎ}x\left(A\cap R^{-1}\left[\left\{X\right\}\right]\right)$$
9	4 8	nfcxfr	$$⊢\underset{\_}{Ⅎ}xPred\left(R,A,X\right)$$