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

Theorem dmun 5003
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 3683 . . 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 4415 . . . . . 6  |-  ( y ( A  u.  B
) x  <->  ( y A x  \/  y B x ) )
32exbii 1712 . . . . 5  |-  ( E. x  y ( A  u.  B ) x  <->  E. x ( y A x  \/  y B x ) )
4 19.43 1739 . . . . 5  |-  ( E. x ( y A x  \/  y B x )  <->  ( E. x  y A x  \/  E. x  y B x ) )
53, 4bitr2i 253 . . . 4  |-  ( ( E. x  y A x  \/  E. x  y B x )  <->  E. x  y ( A  u.  B ) x )
65abbii 2544 . . 3  |-  { y  |  ( E. x  y A x  \/  E. x  y B x ) }  =  {
y  |  E. x  y ( A  u.  B ) x }
71, 6eqtri 2450 . 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 4806 . . 3  |-  dom  A  =  { y  |  E. x  y A x }
9 df-dm 4806 . . 3  |-  dom  B  =  { y  |  E. x  y B x }
108, 9uneq12i 3561 . 2  |-  ( dom 
A  u.  dom  B
)  =  ( { y  |  E. x  y A x }  u.  { y  |  E. x  y B x } )
11 df-dm 4806 . 2  |-  dom  ( A  u.  B )  =  { y  |  E. x  y ( A  u.  B ) x }
127, 10, 113eqtr4ri 2461 1  |-  dom  ( A  u.  B )  =  ( dom  A  u.  dom  B )
Colors of variables: wff setvar class
Syntax hints:    \/ wo 369    = wceq 1437   E.wex 1657   {cab 2414    u. cun 3377   class class class wbr 4366   dom cdm 4796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-un 3384  df-br 4367  df-dm 4806
This theorem is referenced by:  rnun  5206  dmpropg  5271  dmtpop  5274  fntpg  5599  fnun  5643  wfrlem13  7003  wfrlem16  7006  tfrlem10  7060  sbthlem5  7639  fodomr  7676  axdc3lem4  8834  hashfun  12557  s4dom  12948  dmtrclfv  13026  strlemor1  15160  strleun  15163  xpsfrnel2  15414  estrreslem2  15966  mvdco  17029  gsumzaddlem  17497  bnj1416  29800  fixun  30625  rclexi  36135  rtrclex  36137  rtrclexi  36141  cnvrcl0  36145  dmtrcl  36147  dfrtrcl5  36149  dfrcl2  36179  dmtrclfvRP  36235
  Copyright terms: Public domain W3C validator