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

Theorem unex 4534
Description: The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.)
Hypotheses
Ref Expression
unex.1  |-  A  e. 
_V
unex.2  |-  B  e. 
_V
Assertion
Ref Expression
unex  |-  ( A  u.  B )  e. 
_V

Proof of Theorem unex
StepHypRef Expression
1 unex.1 . . 3  |-  A  e. 
_V
2 unex.2 . . 3  |-  B  e. 
_V
31, 2unipr 3857 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4233 . . 3  |-  { A ,  B }  e.  _V
54uniex 4532 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2367 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801    u. cun 3163   {cpr 3654   U.cuni 3843
This theorem is referenced by:  tpex  4535  unexb  4536  fvclex  5777  unen  6959  sbthlem10  6996  unxpdomlem3  7085  isinf  7092  findcard2  7114  ac6sfi  7117  pwfilem  7166  fiin  7191  cnfcomlem  7418  trcl  7426  tc2  7443  rankxpu  7564  rankxplim  7565  rankxplim3  7567  r0weon  7656  infxpenlem  7657  dfac4  7765  dfac2  7773  kmlem2  7793  cdafn  7811  cfsmolem  7912  isfin1-3  8028  axdc2lem  8090  axdc3lem4  8095  axcclem  8099  ttukeylem3  8154  gchac  8311  wunex2  8376  wuncval2  8385  inar1  8413  nn0ex  9987  xrex  10367  hashbclem  11406  ccatfn  11443  incexclem  12311  ramub1lem2  13090  prdsval  13371  imasval  13430  ipoval  14273  fpwipodrs  14283  plusffval  14395  staffval  15628  scaffval  15661  lpival  16013  psrval  16126  xrsex  16398  ipffval  16568  leordtval2  16958  1stckgen  17265  dfac14  17328  ptcmpfi  17520  hausflim  17692  flimclslem  17695  alexsubALTlem2  17758  nmfval  18127  icccmplem2  18344  tchex  18665  tchnmfval  18675  taylfval  19754  subfacp1lem3  23728  subfacp1lem5  23730  erdszelem8  23744  axlowdimlem15  24656  axlowdim  24661  basexre  25625  pgapspf  26155  isray2  26256  isray  26257  comppfsc  26410  rrnval  26654  ralxpmap  26864  elrfi  26872  istopclsd  26878  mzpcompact2lem  26932  eldioph2lem1  26942  eldioph2lem2  26943  eldioph4b  26997  diophren  26999  ttac  27232  pwslnmlem2  27298  enfixsn  27360  dfacbasgrp  27376  islindf4  27411  mendval  27594  idomsubgmo  27617  constr3lem1  28391  constr3cyclpe  28409  3v3e3cycl2  28410  bnj918  29112  lsatset  29802  ldualset  29937  pclfinN  30711  dvaset  31816  dvhset  31893  hlhilset  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-rex 2562  df-v 2803  df-dif 3168  df-un 3170  df-nul 3469  df-sn 3659  df-pr 3660  df-uni 3844
  Copyright terms: Public domain W3C validator