Metamath Proof Explorer


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 𝐴