Theorem dmun 5921

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 4308	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)}
2		brun 5194	. . . . . 6 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥))
3	2	exbii 1848	. . . . 5 ⊢ (∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥 ↔ ∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥))
4		19.43 1882	. . . . 5 ⊢ (∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥) ↔ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥))
5	3, 4	bitr2i 276	. . . 4 ⊢ ((∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥) ↔ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥)
6	5	abbii 2809	. . 3 ⊢ {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥}
7	1, 6	eqtri 2765	. 2 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥}
8		df-dm 5695	. . 3 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥}
9		df-dm 5695	. . 3 ⊢ dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}
10	8, 9	uneq12i 4166	. 2 ⊢ (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥})
11		df-dm 5695	. 2 ⊢ dom (𝐴 ∪ 𝐵) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥}
12	7, 10, 11	3eqtr4ri 2776	1 ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵)

Syntax hints:   ∨ wo 848   = wceq 1540  ∃wex 1779  {cab 2714   ∪ cun 3949   class class class wbr 5143  dom cdm 5685

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-br 5144  df-dm 5695

This theorem is referenced by:  rnun  6165  dmpropg  6235  dmtpop  6238  fntpg  6626  fnun  6682  frrlem14  8324  wfrlem13OLD  8361  wfrlem16OLD  8364  tfrlem10  8427  sbthlem5  9127  fodomr  9168  fodomfir  9368  axdc3lem4  10493  hashfun  14476  s4dom  14958  dmtrclfv  15057  strleun  17194  setsdm  17207  estrreslem2  18183  mvdco  19463  gsumzaddlem  19939  cnfldfunALT  21379  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  noextend  27711  noextendseq  27712  nosupbday  27750  nosupbnd1  27759  nosupbnd2  27761  noinfbday  27765  noinfbnd1  27774  noinfbnd2  27776  noetasuplem4  27781  noetainflem4  27785  uhgrun  29091  upgrun  29135  umgrun  29137  vtxdun  29499  wlkp1  29699  eupthp1  30235  bnj1416  35053  fineqvac  35111  satfdm  35374  fmlasuc0  35389  fixun  35910  rclexi  43628  rtrclex  43630  rtrclexi  43634  cnvrcl0  43638  dmtrcl  43640  dfrtrcl5  43642  dfrcl2  43687  dmtrclfvRP  43743