Theorem dmun 5877

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 4274	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)}
2		brun 5161	. . . . . 6 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥))
3	2	exbii 1848	. . . . 5 ⊢ (∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥 ↔ ∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥))
4		19.43 1882	. . . . 5 ⊢ (∃𝑥(𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥) ↔ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥))
5	3, 4	bitr2i 276	. . . 4 ⊢ ((∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥) ↔ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥)
6	5	abbii 2797	. . 3 ⊢ {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥}
7	1, 6	eqtri 2753	. 2 ⊢ ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥}
8		df-dm 5651	. . 3 ⊢ dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥}
9		df-dm 5651	. . 3 ⊢ dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}
10	8, 9	uneq12i 4132	. 2 ⊢ (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥})
11		df-dm 5651	. 2 ⊢ dom (𝐴 ∪ 𝐵) = {𝑦 ∣ ∃𝑥 𝑦(𝐴 ∪ 𝐵)𝑥}
12	7, 10, 11	3eqtr4ri 2764	1 ⊢ dom (𝐴 ∪ 𝐵) = (dom 𝐴 ∪ dom 𝐵)

Syntax hints:   ∨ wo 847   = wceq 1540  ∃wex 1779  {cab 2708   ∪ cun 3915   class class class wbr 5110  dom cdm 5641

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-br 5111  df-dm 5651

This theorem is referenced by:  rnun  6121  dmpropg  6191  dmtpop  6194  fntpg  6579  fnun  6635  frrlem14  8281  tfrlem10  8358  sbthlem5  9061  fodomr  9098  fodomfir  9286  axdc3lem4  10413  hashfun  14409  s4dom  14892  dmtrclfv  14991  strleun  17134  setsdm  17147  estrreslem2  18106  mvdco  19382  gsumzaddlem  19858  cnfldfunALT  21286  cnfldfunALTOLD  21299  noextend  27585  noextendseq  27586  nosupbday  27624  nosupbnd1  27633  nosupbnd2  27635  noinfbday  27639  noinfbnd1  27648  noinfbnd2  27650  noetasuplem4  27655  noetainflem4  27659  uhgrun  29008  upgrun  29052  umgrun  29054  vtxdun  29416  wlkp1  29616  eupthp1  30152  bnj1416  35036  fineqvac  35094  satfdm  35363  fmlasuc0  35378  fixun  35904  rclexi  43611  rtrclex  43613  rtrclexi  43617  cnvrcl0  43621  dmtrcl  43623  dfrtrcl5  43625  dfrcl2  43670  dmtrclfvRP  43726