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

Theorem dmun 5240
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 3852 . . 3 ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)}
2 brun 4627 . . . . . 6 (𝑦(𝐴𝐵)𝑥 ↔ (𝑦𝐴𝑥𝑦𝐵𝑥))
32exbii 1763 . . . . 5 (∃𝑥 𝑦(𝐴𝐵)𝑥 ↔ ∃𝑥(𝑦𝐴𝑥𝑦𝐵𝑥))
4 19.43 1798 . . . . 5 (∃𝑥(𝑦𝐴𝑥𝑦𝐵𝑥) ↔ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥))
53, 4bitr2i 263 . . . 4 ((∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥) ↔ ∃𝑥 𝑦(𝐴𝐵)𝑥)
65abbii 2725 . . 3 {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} = {𝑦 ∣ ∃𝑥 𝑦(𝐴𝐵)𝑥}
71, 6eqtri 2631 . 2 ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ ∃𝑥 𝑦(𝐴𝐵)𝑥}
8 df-dm 5038 . . 3 dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥}
9 df-dm 5038 . . 3 dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}
108, 9uneq12i 3726 . 2 (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥})
11 df-dm 5038 . 2 dom (𝐴𝐵) = {𝑦 ∣ ∃𝑥 𝑦(𝐴𝐵)𝑥}
127, 10, 113eqtr4ri 2642 1 dom (𝐴𝐵) = (dom 𝐴 ∪ dom 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wo 381   = wceq 1474  wex 1694  {cab 2595  cun 3537   class class class wbr 4577  dom cdm 5028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-br 4578  df-dm 5038
This theorem is referenced by:  rnun  5446  dmpropg  5512  dmtpop  5515  fntpg  5848  fnun  5897  wfrlem13  7291  wfrlem16  7294  tfrlem10  7347  sbthlem5  7936  fodomr  7973  axdc3lem4  9135  hashfun  13036  s4dom  13460  dmtrclfv  13553  setsdm  15670  strlemor1  15742  strleun  15745  xpsfrnel2  15994  estrreslem2  16547  mvdco  17634  gsumzaddlem  18090  bnj1416  30167  fixun  30992  rclexi  36737  rtrclex  36739  rtrclexi  36743  cnvrcl0  36747  dmtrcl  36749  dfrtrcl5  36751  dfrcl2  36781  dmtrclfvRP  36837  vtxdun  40691  1wlkp1  40885  eupthp1  41379
  Copyright terms: Public domain W3C validator