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 
|- F/_ x A
Assertion nfrn 
|- F/_ x ran A

Proof

Step Hyp Ref Expression
1 nfrn.1 
 |-  F/_ x A
2 df-rn 
 |-  ran A = dom `' A
3 1 nfcnv 
 |-  F/_ x `' A
4 3 nfdm 
 |-  F/_ x dom `' A
5 2 4 nfcxfr 
 |-  F/_ x ran A