Theorem nfrn

Description: Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypothesis	nfrn.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfrn	$$⊢\underset{\_}{Ⅎ}x\mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		nfrn.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
3	1	nfcnv	$$⊢\underset{\_}{Ⅎ}x{A}^{-1}$$
4	3	nfdm	$$⊢\underset{\_}{Ⅎ}x\mathrm{dom}{A}^{-1}$$
5	2 4	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\mathrm{ran}A$$