Theorem dmun 5874

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		unab 4271	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)}
2		brun 5158	. . . . . 6 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥))
3	2	exbii 1848	. . . . 5 ⊢ (∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥 ↔ ∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥))
4		19.43 1882	. . . . 5 ⊢ (∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥) ↔ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥))
5	3, 4	bitr2i 276	. . . 4 ⊢ ((∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥) ↔ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥)
6	5	abbii 2796	. . 3 ⊢ {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥}
7	1, 6	eqtri 2752	. 2 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥}
8		df-dm 5648	. . 3 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥}
9		df-dm 5648	. . 3 ⊢ dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}
10	8, 9	uneq12i 4129	. 2 ⊢ (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥})
11		df-dm 5648	. 2 ⊢ dom (𝐴 ∪ 𝐵) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥}
12	7, 10, 11	3eqtr4ri 2763	1 ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵)

Syntax hints:   ∨ wo 847   = wceq 1540  ∃wex 1779  {cab 2707   ∪ cun 3912   class class class wbr 5107  dom cdm 5638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-br 5108  df-dm 5648

This theorem is referenced by:  rnun  6118  dmpropg  6188  dmtpop  6191  fntpg  6576  fnun  6632  frrlem14  8278  tfrlem10  8355  sbthlem5  9055  fodomr  9092  fodomfir  9279  axdc3lem4  10406  hashfun  14402  s4dom  14885  dmtrclfv  14984  strleun  17127  setsdm  17140  estrreslem2  18099  mvdco  19375  gsumzaddlem  19851  cnfldfunALT  21279  cnfldfunALTOLD  21292  noextend  27578  noextendseq  27579  nosupbday  27617  nosupbnd1  27626  nosupbnd2  27628  noinfbday  27632  noinfbnd1  27641  noinfbnd2  27643  noetasuplem4  27648  noetainflem4  27652  uhgrun  29001  upgrun  29045  umgrun  29047  vtxdun  29409  wlkp1  29609  eupthp1  30145  bnj1416  35029  fineqvac  35087  satfdm  35356  fmlasuc0  35371  fixun  35897  rclexi  43604  rtrclex  43606  rtrclexi  43610  cnvrcl0  43614  dmtrcl  43616  dfrtrcl5  43618  dfrcl2  43663  dmtrclfvRP  43719