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

Theorem dmun 5625
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 4151 . . 3 ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)}
2 brun 4976 . . . . . 6 (𝑦(𝐴𝐵)𝑥 ↔ (𝑦𝐴𝑥𝑦𝐵𝑥))
32exbii 1811 . . . . 5 (∃𝑥 𝑦(𝐴𝐵)𝑥 ↔ ∃𝑥(𝑦𝐴𝑥𝑦𝐵𝑥))
4 19.43 1846 . . . . 5 (∃𝑥(𝑦𝐴𝑥𝑦𝐵𝑥) ↔ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥))
53, 4bitr2i 268 . . . 4 ((∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥) ↔ ∃𝑥 𝑦(𝐴𝐵)𝑥)
65abbii 2837 . . 3 {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} = {𝑦 ∣ ∃𝑥 𝑦(𝐴𝐵)𝑥}
71, 6eqtri 2795 . 2 ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ ∃𝑥 𝑦(𝐴𝐵)𝑥}
8 df-dm 5413 . . 3 dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥}
9 df-dm 5413 . . 3 dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}
108, 9uneq12i 4019 . 2 (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥})
11 df-dm 5413 . 2 dom (𝐴𝐵) = {𝑦 ∣ ∃𝑥 𝑦(𝐴𝐵)𝑥}
127, 10, 113eqtr4ri 2806 1 dom (𝐴𝐵) = (dom 𝐴 ∪ dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 834   = wceq 1508  wex 1743  {cab 2751  cun 3820   class class class wbr 4925  dom cdm 5403
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-v 3410  df-un 3827  df-br 4926  df-dm 5413
This theorem is referenced by:  rnun  5841  dmpropg  5908  dmtpop  5911  fntpg  6244  fnun  6293  wfrlem13  7769  wfrlem16  7772  tfrlem10  7825  sbthlem5  8425  fodomr  8462  axdc3lem4  9671  hashfun  13609  s4dom  14141  dmtrclfv  14237  setsdm  16371  strleun  16445  xpsfrnel2cda  16698  estrreslem2  17258  mvdco  18346  gsumzaddlem  18806  cnfldfun  20274  uhgrun  26577  upgrun  26621  umgrun  26623  vtxdun  26981  wlkp1  27184  eupthp1  27761  bnj1416  31988  fmlasuc0  32231  frrlem14  32694  noextend  32731  noextendseq  32732  nosupbday  32763  nosupbnd1  32772  nosupbnd2  32774  noetalem3  32777  noetalem4  32778  fixun  32928  rclexi  39376  rtrclex  39378  rtrclexi  39382  cnvrcl0  39386  dmtrcl  39388  dfrtrcl5  39390  dfrcl2  39420  dmtrclfvRP  39476
  Copyright terms: Public domain W3C validator