Theorem dmun 5859

Description: The domain of a union is the union of domains. Exercise 56(a) of [Enderton] p. 65. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
dmun	⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵)

Proof of Theorem dmun

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

Step	Hyp	Ref	Expression
1		breq1 5089	. . . . 5 ⊢ (𝑦 = 𝑧 → (𝑦𝐴𝑥 ↔ 𝑧𝐴𝑥))
2	1	exbidv 1923	. . . 4 ⊢ (𝑦 = 𝑧 → (∃𝑥 𝑦𝐴𝑥 ↔ ∃𝑥 𝑧𝐴𝑥))
3		breq1 5089	. . . . 5 ⊢ (𝑦 = 𝑧 → (𝑦𝐵𝑥 ↔ 𝑧𝐵𝑥))
4	3	exbidv 1923	. . . 4 ⊢ (𝑦 = 𝑧 → (∃𝑥 𝑦𝐵𝑥 ↔ ∃𝑥 𝑧𝐵𝑥))
5	2, 4	unabw 4248	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑧 ∣ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥)}
6		brun 5137	. . . . . 6 ⊢ (𝑧(𝐴 ∪ 𝐵)𝑥 ↔ (𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥))
7	6	exbii 1850	. . . . 5 ⊢ (∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥 ↔ ∃𝑥(𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥))
8		19.43 1884	. . . . 5 ⊢ (∃𝑥(𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥) ↔ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥))
9	7, 8	bitr2i 276	. . . 4 ⊢ ((∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥) ↔ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥)
10	9	abbii 2804	. . 3 ⊢ {𝑧 ∣ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥)} = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
11	5, 10	eqtri 2760	. 2 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
12		df-dm 5634	. . 3 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥}
13		df-dm 5634	. . 3 ⊢ dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}
14	12, 13	uneq12i 4107	. 2 ⊢ (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥})
15		df-dm 5634	. 2 ⊢ dom (𝐴 ∪ 𝐵) = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
16	11, 14, 15	3eqtr4ri 2771	1 ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵)

Syntax hints:   ∨ wo 848   = wceq 1542  ∃wex 1781  {cab 2715   ∪ cun 3888   class class class wbr 5086  dom cdm 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-dm 5634

This theorem is referenced by:  rnun  6103  dmpropg  6173  dmtpop  6176  fntpg  6552  fnun  6606  frrlem14  8242  tfrlem10  8319  sbthlem5  9022  fodomr  9059  fodomfir  9231  axdc3lem4  10366  hashfun  14390  s4dom  14872  dmtrclfv  14971  strleun  17118  setsdm  17131  estrreslem2  18095  mvdco  19411  gsumzaddlem  19887  cnfldfunALT  21359  cnfldfunALTOLD  21372  noextend  27644  noextendseq  27645  nosupbday  27683  nosupbnd1  27692  nosupbnd2  27694  noinfbday  27698  noinfbnd1  27707  noinfbnd2  27709  noetasuplem4  27714  noetainflem4  27718  uhgrun  29157  upgrun  29201  umgrun  29203  vtxdun  29565  wlkp1  29763  eupthp1  30301  bnj1416  35197  fineqvac  35276  satfdm  35567  fmlasuc0  35582  fixun  36105  dmuncnvepres  38726  dfsucmap3  38798  rclexi  44060  rtrclex  44062  rtrclexi  44066  cnvrcl0  44070  dmtrcl  44072  dfrtrcl5  44074  dfrcl2  44119  dmtrclfvRP  44175