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 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfrn.1 | ⊢ Ⅎ 𝑥 𝐴 | |
2 | df-rn | ⊢ ran 𝐴 = dom ◡ 𝐴 | |
3 | 1 | nfcnv | ⊢ Ⅎ 𝑥 ◡ 𝐴 |
4 | 3 | nfdm | ⊢ Ⅎ 𝑥 dom ◡ 𝐴 |
5 | 2 4 | nfcxfr | ⊢ Ⅎ 𝑥 ran 𝐴 |