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

Theorem dmun 5017
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 3552 . . 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 4200 . . . . . 6  |-  ( y ( A  u.  B
) x  <->  ( y A x  \/  y B x ) )
32exbii 1589 . . . . 5  |-  ( E. x  y ( A  u.  B ) x  <->  E. x ( y A x  \/  y B x ) )
4 19.43 1612 . . . . 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 2500 . . 3  |-  { y  |  ( E. x  y A x  \/  E. x  y B x ) }  =  {
y  |  E. x  y ( A  u.  B ) x }
71, 6eqtri 2408 . 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 4829 . . 3  |-  dom  A  =  { y  |  E. x  y A x }
9 df-dm 4829 . . 3  |-  dom  B  =  { y  |  E. x  y B x }
108, 9uneq12i 3443 . 2  |-  ( dom 
A  u.  dom  B
)  =  ( { y  |  E. x  y A x }  u.  { y  |  E. x  y B x } )
11 df-dm 4829 . 2  |-  dom  ( A  u.  B )  =  { y  |  E. x  y ( A  u.  B ) x }
127, 10, 113eqtr4ri 2419 1  |-  dom  ( A  u.  B )  =  ( dom  A  u.  dom  B )
Colors of variables: wff set class
Syntax hints:    \/ wo 358   E.wex 1547    = wceq 1649   {cab 2374    u. cun 3262   class class class wbr 4154   dom cdm 4819
This theorem is referenced by:  rnun  5221  dmpropg  5284  dmtpop  5287  fntpg  5447  fnun  5492  tfrlem10  6585  sbthlem5  7158  fodomr  7195  axdc3lem4  8267  hashfun  11628  s4dom  11794  strlemor1  13484  strleun  13487  xpsfrnel2  13718  wfrlem13  25293  wfrlem16  25296  fixun  25474  mvdco  27058  bnj1416  28747
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-un 3269  df-br 4155  df-dm 4829
  Copyright terms: Public domain W3C validator