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

Theorem dmun 5049
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 3620 . . 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 4343 . . . . . 6  |-  ( y ( A  u.  B
) x  <->  ( y A x  \/  y B x ) )
32exbii 1634 . . . . 5  |-  ( E. x  y ( A  u.  B ) x  <->  E. x ( y A x  \/  y B x ) )
4 19.43 1660 . . . . 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 2558 . . 3  |-  { y  |  ( E. x  y A x  \/  E. x  y B x ) }  =  {
y  |  E. x  y ( A  u.  B ) x }
71, 6eqtri 2463 . 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 4853 . . 3  |-  dom  A  =  { y  |  E. x  y A x }
9 df-dm 4853 . . 3  |-  dom  B  =  { y  |  E. x  y B x }
108, 9uneq12i 3511 . 2  |-  ( dom 
A  u.  dom  B
)  =  ( { y  |  E. x  y A x }  u.  { y  |  E. x  y B x } )
11 df-dm 4853 . 2  |-  dom  ( A  u.  B )  =  { y  |  E. x  y ( A  u.  B ) x }
127, 10, 113eqtr4ri 2474 1  |-  dom  ( A  u.  B )  =  ( dom  A  u.  dom  B )
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    = wceq 1369   E.wex 1586   {cab 2429    u. cun 3329   class class class wbr 4295   dom cdm 4843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-un 3336  df-br 4296  df-dm 4853
This theorem is referenced by:  rnun  5248  dmpropg  5315  dmtpop  5318  fntpg  5476  fnun  5520  tfrlem10  6849  sbthlem5  7428  fodomr  7465  axdc3lem4  8625  hashfun  12202  s4dom  12532  strlemor1  14268  strleun  14271  xpsfrnel2  14506  mvdco  15954  gsumzaddlem  16411  wfrlem13  27739  wfrlem16  27742  fixun  27943  bnj1416  32033
  Copyright terms: Public domain W3C validator