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

Theorem unex 6547
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 4175 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4606 . . 3  |-  { A ,  B }  e.  _V
54uniex 6545 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2503 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872   _Vcvv 3022    u. cun 3377   {cpr 3943   U.cuni 4162
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603  ax-un 6541
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-rex 2720  df-v 3024  df-dif 3382  df-un 3384  df-nul 3705  df-sn 3942  df-pr 3944  df-uni 4163
This theorem is referenced by:  tpex  6548  unexb  6549  fvclex  6723  ralxpmap  7476  unen  7606  enfixsn  7634  sbthlem10  7644  unxpdomlem3  7731  isinf  7738  findcard2  7764  ac6sfi  7768  pwfilem  7821  fiin  7889  cnfcomlem  8156  trcl  8164  tc2  8178  rankxpu  8299  rankxplim  8302  rankxplim3  8304  r0weon  8395  infxpenlem  8396  dfac4  8504  dfac2  8512  kmlem2  8532  cdafn  8550  cfsmolem  8651  isfin1-3  8767  axdc2lem  8829  axdc3lem4  8834  axcclem  8838  ttukeylem3  8892  gchac  9057  wunex2  9114  wuncval2  9123  inar1  9151  nn0ex  10826  xrex  11250  hashbclem  12563  ccatfnOLD  12666  incexclem  13837  ramub1lem2  14928  prdsval  15296  imasval  15354  imasvalOLD  15355  ipoval  16343  fpwipodrs  16353  plusffval  16436  staffval  18018  scaffval  18052  lpival  18412  psrval  18529  xrsex  18926  ipffval  19157  islindf4  19338  neitr  20138  leordtval2  20170  comppfsc  20489  1stckgen  20511  dfac14  20575  ptcmpfi  20770  hausflim  20938  flimclslem  20941  alexsubALTlem2  21005  nmfval  21545  icccmplem2  21783  tchex  22133  tchnmfval  22144  taylfval  23256  legval  24571  axlowdimlem15  24928  axlowdim  24933  eengv  24951  constr3lem1  25315  constr3cyclpe  25333  3v3e3cycl2  25334  padct  28257  ordtconlem1  28682  sxbrsigalem2  29060  bnj918  29529  subfacp1lem3  29857  subfacp1lem5  29859  erdszelem8  29873  mrexval  30091  mrsubcv  30100  mrsubff  30102  mrsubccat  30108  elmrsubrn  30110  finixpnum  31837  poimirlem4  31851  poimirlem15  31862  poimirlem28  31875  rrnval  32066  lsatset  32468  ldualset  32603  pclfinN  33377  dvaset  34484  dvhset  34561  hlhilset  35417  elrfi  35448  istopclsd  35454  mzpcompact2lem  35505  eldioph2lem1  35514  eldioph2lem2  35515  eldioph4b  35566  diophren  35568  ttac  35804  pwslnmlem2  35864  dfacbasgrp  35880  mendval  35962  idomsubgmo  35985  superuncl  36085  ssuncl  36087  sssymdifcl  36089  rclexi  36135  trclexi  36140  rtrclexi  36141  dfrtrcl5  36149  dfrcl2  36179  comptiunov2i  36211  cotrclrcl  36247  frege83  36455  frege110  36482  frege133  36505  fnchoice  37266  limcresiooub  37606  limcresioolb  37607  fourierdlem48  37901  fourierdlem49  37902  fourierdlem102  37955  fourierdlem114  37967  sge0resplit  38099  uhgrunop  38944  upgrunop  38979  umgrunop  38981
  Copyright terms: Public domain W3C validator