Theorem dmun 5890

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 5107	. . . . 5 ⊢ (𝑦 = 𝑧 → (𝑦𝐴𝑥 ↔ 𝑧𝐴𝑥))
2	1	exbidv 1944	. . . 4 ⊢ (𝑦 = 𝑧 → (∃𝑥 𝑦𝐴𝑥 ↔ ∃𝑥 𝑧𝐴𝑥))
3		breq1 5107	. . . . 5 ⊢ (𝑦 = 𝑧 → (𝑦𝐵𝑥 ↔ 𝑧𝐵𝑥))
4	3	exbidv 1944	. . . 4 ⊢ (𝑦 = 𝑧 → (∃𝑥 𝑦𝐵𝑥 ↔ ∃𝑥 𝑧𝐵𝑥))
5	2, 4	unabw 4262	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑧 ∣ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥)}
6		brun 5155	. . . . . 6 ⊢ (𝑧(𝐴 ∪ 𝐵)𝑥 ↔ (𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥))
7	6	exbii 1871	. . . . 5 ⊢ (∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥 ↔ ∃𝑥(𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥))
8		19.43 1905	. . . . 5 ⊢ (∃𝑥(𝑧𝐴𝑥 ∨ 𝑧𝐵𝑥) ↔ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥))
9	7, 8	bitr2i 279	. . . 4 ⊢ ((∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥) ↔ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥)
10	9	abbii 2832	. . 3 ⊢ {𝑧 ∣ (∃𝑥 𝑧𝐴𝑥 ∨ ∃𝑥 𝑧𝐵𝑥)} = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
11	5, 10	eqtri 2788	. 2 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
12		df-dm 5661	. . 3 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥}
13		df-dm 5661	. . 3 ⊢ dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}
14	12, 13	uneq12i 4122	. 2 ⊢ (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥})
15		df-dm 5661	. 2 ⊢ dom (𝐴 ∪ 𝐵) = {𝑧 ∣ ∃𝑥 𝑧(𝐴 ∪ 𝐵)𝑥}
16	11, 14, 15	3eqtr4ri 2799	1 ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵)

Syntax hints:   ∨ wo 860   = wceq 1563  ∃wex 1802  {cab 2743   ∪ cun 3905   class class class wbr 5104  dom cdm 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-dm 5661

This theorem is referenced by:  rnun  6132  dmpropg  6205  dmtpop  6208  fntpg  6585  fnun  6639  frrlem14  8284  tfrlem10  8362  sbthlem5  9067  fodomr  9104  fodomfir  9275  axdc3lem4  10425  hashfun  14462  s4dom  14944  dmtrclfv  15043  strleun  17205  setsdm  17218  estrreslem2  18182  mvdco  19503  gsumzaddlem  19979  cnfldfunALT  21494  noextend  27784  noextendseq  27785  nosupbday  27823  nosupbnd1  27832  nosupbnd2  27834  noinfbday  27838  noinfbnd1  27847  noinfbnd2  27849  noetasuplem4  27854  noetainflem4  27858  uhgrun  29329  upgrun  29373  umgrun  29375  vtxdun  29736  wlkp1  29934  eupthp1  30472  bnj1416  35339  fineqvac  35419  satfdm  35727  fmlasuc0  35742  fixun  36265  dmuncnvepres  38897  dfsucmap3  38969  rclexi  44198  rtrclex  44200  rtrclexi  44204  cnvrcl0  44208  dmtrcl  44210  dfrtrcl5  44212  dfrcl2  44257  dmtrclfvRP  44313