This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ _ x A
Assertion nfrn ⊢ Ⅎ _ x ran ⁡ A

Proof

Step Hyp Ref Expression
1 nfrn.1 ⊢ Ⅎ _ x A
2 df-rn ⊢ ran ⁡ A = dom ⁡ A -1
3 1 nfcnv ⊢ Ⅎ _ x A -1
4 3 nfdm ⊢ Ⅎ _ x dom ⁡ A -1
5 2 4 nfcxfr ⊢ Ⅎ _ x ran ⁡ A