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

Metamath Proof Explorer

Theorem dfrnf

Description: Definition of range, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Aug-1995) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses dfrnf.1 ⊢ Ⅎ _ x A
dfrnf.2 ⊢ Ⅎ _ y A
Assertion dfrnf ⊢ ran ⁡ A = y | ∃ x x A y

Proof

Step Hyp Ref Expression
1 dfrnf.1 ⊢ Ⅎ _ x A
2 dfrnf.2 ⊢ Ⅎ _ y A
3 dfrn2 ⊢ ran ⁡ A = w | ∃ v v A w
4 nfcv ⊢ Ⅎ _ x v
5 nfcv ⊢ Ⅎ _ x w
6 4 1 5 nfbr ⊢ Ⅎ x v A w
7 nfv ⊢ Ⅎ v x A w
8 breq1 ⊢ v = x → v A w ↔ x A w
9 6 7 8 cbvexv1 ⊢ ∃ v v A w ↔ ∃ x x A w
10 9 abbii ⊢ w | ∃ v v A w = w | ∃ x x A w
11 nfcv ⊢ Ⅎ _ y x
12 nfcv ⊢ Ⅎ _ y w
13 11 2 12 nfbr ⊢ Ⅎ y x A w
14 13 nfex ⊢ Ⅎ y ∃ x x A w
15 nfv ⊢ Ⅎ w ∃ x x A y
16 breq2 ⊢ w = y → x A w ↔ x A y
17 16 exbidv ⊢ w = y → ∃ x x A w ↔ ∃ x x A y
18 14 15 17 cbvabw ⊢ w | ∃ x x A w = y | ∃ x x A y
19 3 10 18 3eqtri ⊢ ran ⁡ A = y | ∃ x x A y