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

Theorem dmun 4885
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 )
Dummy variables  x  y are mutually distinct and distinct from all other variables.

Proof of Theorem dmun
StepHypRef Expression
1 unab 3437 . . 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 4071 . . . . . 6  |-  ( y ( A  u.  B
) x  <->  ( y A x  \/  y B x ) )
32exbii 1570 . . . . 5  |-  ( E. x  y ( A  u.  B ) x  <->  E. x ( y A x  \/  y B x ) )
4 19.43 1593 . . . . 5  |-  ( E. x ( y A x  \/  y B x )  <->  ( E. x  y A x  \/  E. x  y B x ) )
53, 4bitr2i 243 . . . 4  |-  ( ( E. x  y A x  \/  E. x  y B x )  <->  E. x  y ( A  u.  B ) x )
65abbii 2397 . . 3  |-  { y  |  ( E. x  y A x  \/  E. x  y B x ) }  =  {
y  |  E. x  y ( A  u.  B ) x }
71, 6eqtri 2305 . 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 4699 . . 3  |-  dom  A  =  { y  |  E. x  y A x }
9 df-dm 4699 . . 3  |-  dom  B  =  { y  |  E. x  y B x }
108, 9uneq12i 3329 . 2  |-  ( dom 
A  u.  dom  B
)  =  ( { y  |  E. x  y A x }  u.  { y  |  E. x  y B x } )
11 df-dm 4699 . 2  |-  dom  (  A  u.  B )  =  { y  |  E. x  y ( A  u.  B ) x }
127, 10, 113eqtr4ri 2316 1  |-  dom  (  A  u.  B )  =  ( dom  A  u.  dom  B )
Colors of variables: wff set class
Syntax hints:    \/ wo 359   E.wex 1529    = wceq 1624   {cab 2271    u. cun 3152   class class class wbr 4025   dom cdm 4689
This theorem is referenced by:  rnun  5089  dmpropg  5145  dmtpop  5148  fnun  5316  tfrlem10  6399  sbthlem5  6971  fodomr  7008  axdc3lem4  8075  hashfun  11384  strlemor1  13230  strleun  13233  xpsfrnel2  13462  wfrlem13  23670  wfrlem16  23673  fixun  23858  mvdco  26788  bnj1416  28337
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-un 3159  df-br 4026  df-dm 4699
  Copyright terms: Public domain W3C validator