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

Theorem dmun 5219
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  ( A  u.  B )  =  ( dom  A  u.  dom  B )

Proof of Theorem dmun
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unab 3772 . . 3  |-  ( { y  |  E. x  y A x }  u.  { y  |  E. x  y B x } )  =  { y  |  ( E. x  y A x  \/  E. x  y B x ) }
2 brun 4504 . . . . . 6  |-  ( y ( A  u.  B
) x  <->  ( y A x  \/  y B x ) )
32exbii 1668 . . . . 5  |-  ( E. x  y ( A  u.  B ) x  <->  E. x ( y A x  \/  y B x ) )
4 19.43 1694 . . . . 5  |-  ( E. x ( y A x  \/  y B x )  <->  ( E. x  y A x  \/  E. x  y B x ) )
53, 4bitr2i 250 . . . 4  |-  ( ( E. x  y A x  \/  E. x  y B x )  <->  E. x  y ( A  u.  B ) x )
65abbii 2591 . . 3  |-  { y  |  ( E. x  y A x  \/  E. x  y B x ) }  =  {
y  |  E. x  y ( A  u.  B ) x }
71, 6eqtri 2486 . 2  |-  ( { y  |  E. x  y A x }  u.  { y  |  E. x  y B x } )  =  { y  |  E. x  y ( A  u.  B ) x }
8 df-dm 5018 . . 3  |-  dom  A  =  { y  |  E. x  y A x }
9 df-dm 5018 . . 3  |-  dom  B  =  { y  |  E. x  y B x }
108, 9uneq12i 3652 . 2  |-  ( dom 
A  u.  dom  B
)  =  ( { y  |  E. x  y A x }  u.  { y  |  E. x  y B x } )
11 df-dm 5018 . 2  |-  dom  ( A  u.  B )  =  { y  |  E. x  y ( A  u.  B ) x }
127, 10, 113eqtr4ri 2497 1  |-  dom  ( A  u.  B )  =  ( dom  A  u.  dom  B )
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    = wceq 1395   E.wex 1613   {cab 2442    u. cun 3469   class class class wbr 4456   dom cdm 5008
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3476  df-br 4457  df-dm 5018
This theorem is referenced by:  rnun  5421  dmpropg  5487  dmtpop  5490  fntpg  5649  fnun  5693  tfrlem10  7074  sbthlem5  7650  fodomr  7687  axdc3lem4  8850  hashfun  12499  s4dom  12879  strlemor1  14739  strleun  14742  xpsfrnel2  14982  estrreslem2  15534  mvdco  16597  gsumzaddlem  17061  wfrlem13  29551  wfrlem16  29554  fixun  29743  bnj1416  34217
  Copyright terms: Public domain W3C validator