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

Theorem dmun 5214
 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

Proof of Theorem dmun
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unab 3764 . . 3
2 brun 4500 . . . . . 6
32exbii 1667 . . . . 5
4 19.43 1693 . . . . 5
53, 4bitr2i 250 . . . 4
65abbii 2591 . . 3
71, 6eqtri 2486 . 2
8 df-dm 5014 . . 3
9 df-dm 5014 . . 3
108, 9uneq12i 3655 . 2
11 df-dm 5014 . 2
127, 10, 113eqtr4ri 2497 1
 Colors of variables: wff setvar class Syntax hints:  \/wo 368  =wceq 1395  E.wex 1612  {cab 2442  u.cun 3473   class class class wbr 4452  domcdm 5004 This theorem is referenced by:  rnun  5419  dmpropg  5486  dmtpop  5489  fntpg  5648  fnun  5692  tfrlem10  7075  sbthlem5  7651  fodomr  7688  axdc3lem4  8854  hashfun  12495  s4dom  12867  strlemor1  14724  strleun  14727  xpsfrnel2  14962  mvdco  16470  gsumzaddlem  16934  wfrlem13  29355  wfrlem16  29358  fixun  29559  estrreslem2  32644  bnj1416  34095 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-br 4453  df-dm 5014
 Copyright terms: Public domain W3C validator