MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmun Structured version   Visualization version   GIF version

Theorem dmun 5867
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.
StepHypRef Expression
1 unab 4259 . . 3 ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)}
2 brun 5157 . . . . . 6 (𝑦(𝐴𝐵)𝑥 ↔ (𝑦𝐴𝑥𝑦𝐵𝑥))
32exbii 1851 . . . . 5 (∃𝑥 𝑦(𝐴𝐵)𝑥 ↔ ∃𝑥(𝑦𝐴𝑥𝑦𝐵𝑥))
4 19.43 1886 . . . . 5 (∃𝑥(𝑦𝐴𝑥𝑦𝐵𝑥) ↔ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥))
53, 4bitr2i 276 . . . 4 ((∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥) ↔ ∃𝑥 𝑦(𝐴𝐵)𝑥)
65abbii 2803 . . 3 {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} = {𝑦 ∣ ∃𝑥 𝑦(𝐴𝐵)𝑥}
71, 6eqtri 2761 . 2 ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ ∃𝑥 𝑦(𝐴𝐵)𝑥}
8 df-dm 5644 . . 3 dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥}
9 df-dm 5644 . . 3 dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}
108, 9uneq12i 4122 . 2 (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥})
11 df-dm 5644 . 2 dom (𝐴𝐵) = {𝑦 ∣ ∃𝑥 𝑦(𝐴𝐵)𝑥}
127, 10, 113eqtr4ri 2772 1 dom (𝐴𝐵) = (dom 𝐴 ∪ dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 846   = wceq 1542  wex 1782  {cab 2710  cun 3909   class class class wbr 5106  dom cdm 5634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-un 3916  df-br 5107  df-dm 5644
This theorem is referenced by:  rnun  6099  dmpropg  6168  dmtpop  6171  fntpg  6562  fnun  6615  frrlem14  8231  wfrlem13OLD  8268  wfrlem16OLD  8271  tfrlem10  8334  sbthlem5  9034  fodomr  9075  axdc3lem4  10394  hashfun  14343  s4dom  14814  dmtrclfv  14909  strleun  17034  setsdm  17047  estrreslem2  18031  mvdco  19232  gsumzaddlem  19703  cnfldfunALT  20825  cnfldfunALTOLD  20826  noextend  27030  noextendseq  27031  nosupbday  27069  nosupbnd1  27078  nosupbnd2  27080  noinfbday  27084  noinfbnd1  27093  noinfbnd2  27095  noetasuplem4  27100  noetainflem4  27104  uhgrun  28067  upgrun  28111  umgrun  28113  vtxdun  28471  wlkp1  28671  eupthp1  29202  bnj1416  33708  fineqvac  33755  satfdm  34020  fmlasuc0  34035  fixun  34540  rclexi  41975  rtrclex  41977  rtrclexi  41981  cnvrcl0  41985  dmtrcl  41987  dfrtrcl5  41989  dfrcl2  42034  dmtrclfvRP  42090
  Copyright terms: Public domain W3C validator