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

Theorem unex 6393
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 4119 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4549 . . 3  |-  { A ,  B }  e.  _V
54uniex 6391 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2514 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   _Vcvv 2987    u. cun 3341   {cpr 3894   U.cuni 4106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4428  ax-nul 4436  ax-pr 4546  ax-un 6387
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-rex 2736  df-v 2989  df-dif 3346  df-un 3348  df-nul 3653  df-sn 3893  df-pr 3895  df-uni 4107
This theorem is referenced by:  tpex  6394  unexb  6395  fvclex  6564  ralxpmap  7277  unen  7407  enfixsn  7435  sbthlem10  7445  unxpdomlem3  7534  isinf  7541  findcard2  7567  ac6sfi  7571  pwfilem  7620  fiin  7687  cnfcomlem  7947  cnfcomlemOLD  7955  trcl  7963  tc2  7977  rankxpu  8098  rankxplim  8101  rankxplim3  8103  r0weon  8194  infxpenlem  8195  dfac4  8307  dfac2  8315  kmlem2  8335  cdafn  8353  cfsmolem  8454  isfin1-3  8570  axdc2lem  8632  axdc3lem4  8637  axcclem  8641  ttukeylem3  8695  gchac  8863  wunex2  8920  wuncval2  8929  inar1  8957  nn0ex  10600  xrex  11003  hashbclem  12220  ccatfn  12287  incexclem  13314  ramub1lem2  14103  prdsval  14408  imasval  14464  ipoval  15339  fpwipodrs  15349  plusffval  15442  staffval  16947  scaffval  16981  lpival  17342  psrval  17444  xrsex  17846  ipffval  18092  islindf4  18282  neitr  18799  leordtval2  18831  1stckgen  19142  dfac14  19206  ptcmpfi  19401  hausflim  19569  flimclslem  19572  alexsubALTlem2  19635  nmfval  20196  icccmplem2  20415  tchex  20747  tchnmfval  20758  taylfval  21839  legval  23030  axlowdimlem15  23217  axlowdim  23222  eengv  23240  constr3lem1  23546  constr3cyclpe  23564  3v3e3cycl2  23565  gsumle  26261  ordtconlem1  26369  sxbrsigalem2  26716  subfacp1lem3  27085  subfacp1lem5  27087  erdszelem8  27101  finixpnum  28433  comppfsc  28598  rrnval  28745  elrfi  29049  istopclsd  29055  mzpcompact2lem  29107  eldioph2lem1  29117  eldioph2lem2  29118  eldioph4b  29169  diophren  29171  ttac  29404  pwslnmlem2  29465  dfacbasgrp  29483  mendval  29559  idomsubgmo  29582  fnchoice  29770  bnj918  31778  lsatset  32654  ldualset  32789  pclfinN  33563  dvaset  34668  dvhset  34745  hlhilset  35601
  Copyright terms: Public domain W3C validator