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

Theorem unex 4666
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 3989 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4366 . . 3  |-  { A ,  B }  e.  _V
54uniex 4664 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2475 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2916    u. cun 3278   {cpr 3775   U.cuni 3975
This theorem is referenced by:  tpex  4667  unexb  4668  fvclex  5940  unen  7148  sbthlem10  7185  unxpdomlem3  7274  isinf  7281  findcard2  7307  ac6sfi  7310  pwfilem  7359  fiin  7385  cnfcomlem  7612  trcl  7620  tc2  7637  rankxpu  7758  rankxplim  7759  rankxplim3  7761  r0weon  7850  infxpenlem  7851  dfac4  7959  dfac2  7967  kmlem2  7987  cdafn  8005  cfsmolem  8106  isfin1-3  8222  axdc2lem  8284  axdc3lem4  8289  axcclem  8293  ttukeylem3  8347  gchac  8504  wunex2  8569  wuncval2  8578  inar1  8606  nn0ex  10183  xrex  10565  hashbclem  11656  ccatfn  11696  incexclem  12571  ramub1lem2  13350  prdsval  13633  imasval  13692  ipoval  14535  fpwipodrs  14545  plusffval  14657  staffval  15890  scaffval  15923  lpival  16271  psrval  16384  xrsex  16671  ipffval  16834  neitr  17198  leordtval2  17230  1stckgen  17539  dfac14  17603  ptcmpfi  17798  hausflim  17966  flimclslem  17969  alexsubALTlem2  18032  nmfval  18589  icccmplem2  18807  tchex  19129  tchnmfval  19139  taylfval  20228  constr3lem1  21585  constr3cyclpe  21603  3v3e3cycl2  21604  sxbrsigalem2  24589  subfacp1lem3  24821  subfacp1lem5  24823  erdszelem8  24837  axlowdimlem15  25799  axlowdim  25804  comppfsc  26277  rrnval  26426  ralxpmap  26632  elrfi  26638  istopclsd  26644  mzpcompact2lem  26698  eldioph2lem1  26708  eldioph2lem2  26709  eldioph4b  26762  diophren  26764  ttac  26997  pwslnmlem2  27063  enfixsn  27125  dfacbasgrp  27141  islindf4  27176  mendval  27359  idomsubgmo  27382  fnchoice  27567  bnj918  28841  lsatset  29473  ldualset  29608  pclfinN  30382  dvaset  31487  dvhset  31564  hlhilset  32420
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 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363  ax-un 4660
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-rex 2672  df-v 2918  df-dif 3283  df-un 3285  df-nul 3589  df-sn 3780  df-pr 3781  df-uni 3976
  Copyright terms: Public domain W3C validator