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

Theorem unex 4455
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 3782 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4155 . . 3  |-  { A ,  B }  e.  _V
54uniex 4453 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2327 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2740    u. cun 3092   {cpr 3582   U.cuni 3768
This theorem is referenced by:  tpex  4456  unexb  4457  fvclex  5660  unen  6876  sbthlem10  6913  unxpdomlem3  7002  isinf  7009  findcard2  7031  ac6sfi  7034  pwfilem  7083  fiin  7108  cnfcomlem  7335  trcl  7343  tc2  7360  rankxpu  7481  rankxplim  7482  rankxplim3  7484  r0weon  7573  infxpenlem  7574  dfac4  7682  dfac2  7690  kmlem2  7710  cdafn  7728  cfsmolem  7829  isfin1-3  7945  axdc2lem  8007  axdc3lem4  8012  axcclem  8016  ttukeylem3  8071  gchac  8228  wunex2  8293  wuncval2  8302  inar1  8330  nn0ex  9903  xrex  10283  hashbclem  11320  ccatfn  11357  ramub1lem2  13001  prdsval  13282  imasval  13341  ipoval  14184  fpwipodrs  14194  plusffval  14306  staffval  15539  scaffval  15572  lpival  15924  psrval  16037  xrsex  16309  ipffval  16479  leordtval2  16869  1stckgen  17176  dfac14  17239  ptcmpfi  17431  hausflim  17603  flimclslem  17606  alexsubALTlem2  17669  nmfval  18038  icccmplem2  18255  tchex  18576  tchnmfval  18586  taylfval  19665  subfacp1lem3  23050  subfacp1lem5  23052  erdszelem8  23066  axlowdimlem15  23924  axlowdim  23929  basexre  24854  pgapspf  25384  isray2  25485  isray  25486  comppfsc  25639  rrnval  25883  ralxpmap  26093  elrfi  26101  istopclsd  26107  mzpcompact2lem  26161  eldioph2lem1  26171  eldioph2lem2  26172  eldioph4b  26226  diophren  26228  ttac  26461  pwslnmlem2  26527  enfixsn  26589  dfacbasgrp  26605  islindf4  26640  mendval  26823  idomsubgmo  26846  bnj918  27808  lsatset  28310  ldualset  28445  pclfinN  29219  dvaset  30324  dvhset  30401  hlhilset  31257
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152  ax-un 4449
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-rex 2521  df-v 2742  df-dif 3097  df-un 3099  df-nul 3398  df-sn 3587  df-pr 3588  df-uni 3769
  Copyright terms: Public domain W3C validator