Theorem dmuni 4563

Description: The domain of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 3-Feb-2004.)

Assertion

Ref	Expression
dmuni	⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥

Distinct variable group:   𝑥,𝐴

Proof of Theorem dmuni

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		excom 1594	. . . . 5 ⊢ (∃𝑧∃𝑥(⟨𝑦, 𝑧⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥∃𝑧(⟨𝑦, 𝑧⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴))
2		ancom 262	. . . . . . 7 ⊢ ((∃𝑧⟨𝑦, 𝑧⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑧⟨𝑦, 𝑧⟩ ∈ 𝑥))
3		19.41v 1823	. . . . . . 7 ⊢ (∃𝑧(⟨𝑦, 𝑧⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (∃𝑧⟨𝑦, 𝑧⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴))
4		vex 2604	. . . . . . . . 9 ⊢ 𝑦 ∈ V
5	4	eldm2 4551	. . . . . . . 8 ⊢ (𝑦 ∈ dom 𝑥 ↔ ∃𝑧⟨𝑦, 𝑧⟩ ∈ 𝑥)
6	5	anbi2i 444	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑧⟨𝑦, 𝑧⟩ ∈ 𝑥))
7	2, 3, 6	3bitr4i 210	. . . . . 6 ⊢ (∃𝑧(⟨𝑦, 𝑧⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥))
8	7	exbii 1536	. . . . 5 ⊢ (∃𝑥∃𝑧(⟨𝑦, 𝑧⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥))
9	1, 8	bitri 182	. . . 4 ⊢ (∃𝑧∃𝑥(⟨𝑦, 𝑧⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥))
10		eluni 3604	. . . . 5 ⊢ (⟨𝑦, 𝑧⟩ ∈ ∪ 𝐴 ↔ ∃𝑥(⟨𝑦, 𝑧⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴))
11	10	exbii 1536	. . . 4 ⊢ (∃𝑧⟨𝑦, 𝑧⟩ ∈ ∪ 𝐴 ↔ ∃𝑧∃𝑥(⟨𝑦, 𝑧⟩ ∈ 𝑥 ∧ 𝑥 ∈ 𝐴))
12		df-rex 2354	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝑥))
13	9, 11, 12	3bitr4i 210	. . 3 ⊢ (∃𝑧⟨𝑦, 𝑧⟩ ∈ ∪ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥)
14	4	eldm2 4551	. . 3 ⊢ (𝑦 ∈ dom ∪ 𝐴 ↔ ∃𝑧⟨𝑦, 𝑧⟩ ∈ ∪ 𝐴)
15		eliun 3682	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 dom 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥)
16	13, 14, 15	3bitr4i 210	. 2 ⊢ (𝑦 ∈ dom ∪ 𝐴 ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 dom 𝑥)
17	16	eqriv 2078	1 ⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥

Syntax hints:   ∧ wa 102   = wceq 1284  ∃wex 1421   ∈ wcel 1433  ∃wrex 2349  ⟨cop 3401  ∪ cuni 3601  ∪ ciun 3678  dom cdm 4363

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-iun 3680  df-br 3786  df-dm 4373

This theorem is referenced by:  tfrlem8  5957  tfrlemi14d  5970