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

Metamath Proof Explorer

Theorem dfdmf

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

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

Proof

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