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	⊢ Ⅎ 𝑥 𝐴
Assertion	nfrn	⊢ Ⅎ 𝑥 ran 𝐴

Proof

Step	Hyp	Ref	Expression
1		nfrn.1	⊢ Ⅎ 𝑥 𝐴
2		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
3	1	nfcnv	⊢ Ⅎ 𝑥 ◡ 𝐴
4	3	nfdm	⊢ Ⅎ 𝑥 dom ◡ 𝐴
5	2 4	nfcxfr	⊢ Ⅎ 𝑥 ran 𝐴