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

Theorem unex 6616
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 4225 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4656 . . 3  |-  { A ,  B }  e.  _V
54uniex 6614 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2537 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1898   _Vcvv 3057    u. cun 3414   {cpr 3982   U.cuni 4212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653  ax-un 6610
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-rex 2755  df-v 3059  df-dif 3419  df-un 3421  df-nul 3744  df-sn 3981  df-pr 3983  df-uni 4213
This theorem is referenced by:  tpex  6617  unexb  6618  fvclex  6792  ralxpmap  7547  unen  7678  enfixsn  7707  sbthlem10  7717  unxpdomlem3  7804  isinf  7811  findcard2  7837  ac6sfi  7841  pwfilem  7894  fiin  7962  cnfcomlem  8230  trcl  8238  tc2  8252  rankxpu  8373  rankxplim  8376  rankxplim3  8378  r0weon  8469  infxpenlem  8470  dfac4  8579  dfac2  8587  kmlem2  8607  cdafn  8625  cfsmolem  8726  isfin1-3  8842  axdc2lem  8904  axdc3lem4  8909  axcclem  8913  ttukeylem3  8967  gchac  9132  wunex2  9189  wuncval2  9198  inar1  9226  nn0ex  10904  xrex  11328  hashbclem  12648  ccatfnOLD  12754  incexclem  13943  ramub1lem2  15034  prdsval  15402  imasval  15460  imasvalOLD  15461  ipoval  16449  fpwipodrs  16459  plusffval  16542  staffval  18124  scaffval  18158  lpival  18518  psrval  18635  xrsex  19032  ipffval  19264  islindf4  19445  neitr  20245  leordtval2  20277  comppfsc  20596  1stckgen  20618  dfac14  20682  ptcmpfi  20877  hausflim  21045  flimclslem  21048  alexsubALTlem2  21112  nmfval  21652  icccmplem2  21890  tchex  22240  tchnmfval  22251  taylfval  23363  legval  24678  axlowdimlem15  25035  axlowdim  25040  eengv  25058  constr3lem1  25422  constr3cyclpe  25440  3v3e3cycl2  25441  padct  28356  ordtconlem1  28779  sxbrsigalem2  29157  bnj918  29626  subfacp1lem3  29954  subfacp1lem5  29956  erdszelem8  29970  mrexval  30188  mrsubcv  30197  mrsubff  30199  mrsubccat  30205  elmrsubrn  30207  finixpnum  31975  poimirlem4  31989  poimirlem15  32000  poimirlem28  32013  rrnval  32204  lsatset  32601  ldualset  32736  pclfinN  33510  dvaset  34617  dvhset  34694  hlhilset  35550  elrfi  35581  istopclsd  35587  mzpcompact2lem  35638  eldioph2lem1  35647  eldioph2lem2  35648  eldioph4b  35699  diophren  35701  ttac  35936  pwslnmlem2  35996  dfacbasgrp  36012  mendval  36094  idomsubgmo  36117  superuncl  36217  ssuncl  36219  sssymdifcl  36221  rclexi  36267  trclexi  36272  rtrclexi  36273  dfrtrcl5  36281  dfrcl2  36311  comptiunov2i  36343  cotrclrcl  36379  frege83  36587  frege110  36614  frege133  36637  fnchoice  37390  limcresiooub  37761  limcresioolb  37762  fourierdlem48  38056  fourierdlem49  38057  fourierdlem102  38110  fourierdlem114  38122  sge0resplit  38286  uhgrunop  39215  upgrunop  39255  umgrunop  39257
  Copyright terms: Public domain W3C validator