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 ⊢ Ⅎ 𝑥 𝐴
dfdmf.2 ⊢ Ⅎ 𝑦 𝐴
Assertion dfdmf dom 𝐴 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }

Proof

Step Hyp Ref Expression
1 dfdmf.1 ⊢ Ⅎ 𝑥 𝐴
2 dfdmf.2 ⊢ Ⅎ 𝑦 𝐴
3 df-dm ⊢ dom 𝐴 = { 𝑤 ∣ ∃ 𝑣 𝑤 𝐴 𝑣 }
4 nfcv ⊢ Ⅎ 𝑦 𝑤
5 nfcv ⊢ Ⅎ 𝑦 𝑣
6 4 2 5 nfbr ⊢ Ⅎ 𝑦 𝑤 𝐴 𝑣
7 nfv ⊢ Ⅎ 𝑣 𝑤 𝐴 𝑦
8 breq2 ⊢ ( 𝑣 = 𝑦 → ( 𝑤 𝐴 𝑣 ↔ 𝑤 𝐴 𝑦 ) )
9 6 7 8 cbvexv1 ⊢ ( ∃ 𝑣 𝑤 𝐴 𝑣 ↔ ∃ 𝑦 𝑤 𝐴 𝑦 )
10 9 abbii ⊢ { 𝑤 ∣ ∃ 𝑣 𝑤 𝐴 𝑣 } = { 𝑤 ∣ ∃ 𝑦 𝑤 𝐴 𝑦 }
11 nfcv ⊢ Ⅎ 𝑥 𝑤
12 nfcv ⊢ Ⅎ 𝑥 𝑦
13 11 1 12 nfbr ⊢ Ⅎ 𝑥 𝑤 𝐴 𝑦
14 13 nfex ⊢ Ⅎ 𝑥 ∃ 𝑦 𝑤 𝐴 𝑦
15 nfv ⊢ Ⅎ 𝑤 ∃ 𝑦 𝑥 𝐴 𝑦
16 breq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 𝐴 𝑦 ↔ 𝑥 𝐴 𝑦 ) )
17 16 exbidv ⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑦 𝑤 𝐴 𝑦 ↔ ∃ 𝑦 𝑥 𝐴 𝑦 ) )
18 14 15 17 cbvabw ⊢ { 𝑤 ∣ ∃ 𝑦 𝑤 𝐴 𝑦 } = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }
19 3 10 18 3eqtri ⊢ dom 𝐴 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }