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

Theorem unex 4518
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 3841 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4217 . . 3  |-  { A ,  B }  e.  _V
54uniex 4516 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2354 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788    u. cun 3150   {cpr 3641   U.cuni 3827
This theorem is referenced by:  tpex  4519  unexb  4520  fvclex  5761  unen  6943  sbthlem10  6980  unxpdomlem3  7069  isinf  7076  findcard2  7098  ac6sfi  7101  pwfilem  7150  fiin  7175  cnfcomlem  7402  trcl  7410  tc2  7427  rankxpu  7548  rankxplim  7549  rankxplim3  7551  r0weon  7640  infxpenlem  7641  dfac4  7749  dfac2  7757  kmlem2  7777  cdafn  7795  cfsmolem  7896  isfin1-3  8012  axdc2lem  8074  axdc3lem4  8079  axcclem  8083  ttukeylem3  8138  gchac  8295  wunex2  8360  wuncval2  8369  inar1  8397  nn0ex  9971  xrex  10351  hashbclem  11390  ccatfn  11427  incexclem  12295  ramub1lem2  13074  prdsval  13355  imasval  13414  ipoval  14257  fpwipodrs  14267  plusffval  14379  staffval  15612  scaffval  15645  lpival  15997  psrval  16110  xrsex  16382  ipffval  16552  leordtval2  16942  1stckgen  17249  dfac14  17312  ptcmpfi  17504  hausflim  17676  flimclslem  17679  alexsubALTlem2  17742  nmfval  18111  icccmplem2  18328  tchex  18649  tchnmfval  18659  taylfval  19738  subfacp1lem3  23124  subfacp1lem5  23126  erdszelem8  23140  axlowdimlem15  23995  axlowdim  24000  basexre  24934  pgapspf  25464  isray2  25565  isray  25566  comppfsc  25719  rrnval  25963  ralxpmap  26173  elrfi  26181  istopclsd  26187  mzpcompact2lem  26241  eldioph2lem1  26251  eldioph2lem2  26252  eldioph4b  26306  diophren  26308  ttac  26541  pwslnmlem2  26607  enfixsn  26669  dfacbasgrp  26685  islindf4  26720  mendval  26903  idomsubgmo  26926  bnj918  28169  lsatset  28553  ldualset  28688  pclfinN  29462  dvaset  30567  dvhset  30644  hlhilset  31500
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-rex 2549  df-v 2790  df-dif 3155  df-un 3157  df-nul 3456  df-sn 3646  df-pr 3647  df-uni 3828
  Copyright terms: Public domain W3C validator