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

Theorem dmun 5747
 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 4225 . . 3 ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)}
2 brun 5084 . . . . . 6 (𝑦(𝐴𝐵)𝑥 ↔ (𝑦𝐴𝑥𝑦𝐵𝑥))
32exbii 1849 . . . . 5 (∃𝑥 𝑦(𝐴𝐵)𝑥 ↔ ∃𝑥(𝑦𝐴𝑥𝑦𝐵𝑥))
4 19.43 1883 . . . . 5 (∃𝑥(𝑦𝐴𝑥𝑦𝐵𝑥) ↔ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥))
53, 4bitr2i 279 . . . 4 ((∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥) ↔ ∃𝑥 𝑦(𝐴𝐵)𝑥)
65abbii 2866 . . 3 {𝑦 ∣ (∃𝑥 𝑦𝐴𝑥 ∨ ∃𝑥 𝑦𝐵𝑥)} = {𝑦 ∣ ∃𝑥 𝑦(𝐴𝐵)𝑥}
71, 6eqtri 2824 . 2 ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}) = {𝑦 ∣ ∃𝑥 𝑦(𝐴𝐵)𝑥}
8 df-dm 5533 . . 3 dom 𝐴 = {𝑦 ∣ ∃𝑥 𝑦𝐴𝑥}
9 df-dm 5533 . . 3 dom 𝐵 = {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥}
108, 9uneq12i 4091 . 2 (dom 𝐴 ∪ dom 𝐵) = ({𝑦 ∣ ∃𝑥 𝑦𝐴𝑥} ∪ {𝑦 ∣ ∃𝑥 𝑦𝐵𝑥})
11 df-dm 5533 . 2 dom (𝐴𝐵) = {𝑦 ∣ ∃𝑥 𝑦(𝐴𝐵)𝑥}
127, 10, 113eqtr4ri 2835 1 dom (𝐴𝐵) = (dom 𝐴 ∪ dom 𝐵)
 Colors of variables: wff setvar class Syntax hints:   ∨ wo 844   = wceq 1538  ∃wex 1781  {cab 2779   ∪ cun 3882   class class class wbr 5033  dom cdm 5523 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-br 5034  df-dm 5533 This theorem is referenced by:  rnun  5975  dmpropg  6043  dmtpop  6046  fntpg  6388  fnun  6438  wfrlem13  7954  wfrlem16  7957  tfrlem10  8010  sbthlem5  8619  fodomr  8656  axdc3lem4  9868  hashfun  13798  s4dom  14276  dmtrclfv  14373  setsdm  16513  strleun  16587  estrreslem2  17384  mvdco  18569  gsumzaddlem  19038  cnfldfun  20107  uhgrun  26871  upgrun  26915  umgrun  26917  vtxdun  27275  wlkp1  27475  eupthp1  28005  bnj1416  32425  satfdm  32730  fmlasuc0  32745  frrlem14  33250  noextend  33287  noextendseq  33288  nosupbday  33319  nosupbnd1  33328  nosupbnd2  33330  noetalem3  33333  noetalem4  33334  fixun  33484  rclexi  40308  rtrclex  40310  rtrclexi  40314  cnvrcl0  40318  dmtrcl  40320  dfrtrcl5  40322  dfrcl2  40368  dmtrclfvRP  40424
 Copyright terms: Public domain W3C validator