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

Theorem dmun 5068
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 3600 . . 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 4250 . . . . . 6  |-  ( y ( A  u.  B
) x  <->  ( y A x  \/  y B x ) )
32exbii 1592 . . . . 5  |-  ( E. x  y ( A  u.  B ) x  <->  E. x ( y A x  \/  y B x ) )
4 19.43 1615 . . . . 5  |-  ( E. x ( y A x  \/  y B x )  <->  ( E. x  y A x  \/  E. x  y B x ) )
53, 4bitr2i 242 . . . 4  |-  ( ( E. x  y A x  \/  E. x  y B x )  <->  E. x  y ( A  u.  B ) x )
65abbii 2547 . . 3  |-  { y  |  ( E. x  y A x  \/  E. x  y B x ) }  =  {
y  |  E. x  y ( A  u.  B ) x }
71, 6eqtri 2455 . 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 4880 . . 3  |-  dom  A  =  { y  |  E. x  y A x }
9 df-dm 4880 . . 3  |-  dom  B  =  { y  |  E. x  y B x }
108, 9uneq12i 3491 . 2  |-  ( dom 
A  u.  dom  B
)  =  ( { y  |  E. x  y A x }  u.  { y  |  E. x  y B x } )
11 df-dm 4880 . 2  |-  dom  ( A  u.  B )  =  { y  |  E. x  y ( A  u.  B ) x }
127, 10, 113eqtr4ri 2466 1  |-  dom  ( A  u.  B )  =  ( dom  A  u.  dom  B )
Colors of variables: wff set class
Syntax hints:    \/ wo 358   E.wex 1550    = wceq 1652   {cab 2421    u. cun 3310   class class class wbr 4204   dom cdm 4870
This theorem is referenced by:  rnun  5272  dmpropg  5335  dmtpop  5338  fntpg  5498  fnun  5543  tfrlem10  6640  sbthlem5  7213  fodomr  7250  axdc3lem4  8325  hashfun  11692  s4dom  11858  strlemor1  13548  strleun  13551  xpsfrnel2  13782  wfrlem13  25542  wfrlem16  25545  fixun  25746  mvdco  27356  bnj1416  29345
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-br 4205  df-dm 4880
  Copyright terms: Public domain W3C validator