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

Theorem unex 4409
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 3741 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4111 . . 3  |-  { A ,  B }  e.  _V
54uniex 4407 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2324 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2727    u. cun 3076   {cpr 3545   U.cuni 3727
This theorem is referenced by:  tpex  4410  unexb  4411  fvclex  5613  unen  6828  sbthlem10  6865  unxpdomlem3  6954  isinf  6961  findcard2  6983  ac6sfi  6986  pwfilem  7034  fiin  7059  cnfcomlem  7286  trcl  7294  tc2  7311  rankxpu  7432  rankxplim  7433  rankxplim3  7435  r0weon  7524  infxpenlem  7525  dfac4  7633  dfac2  7641  kmlem2  7661  cdafn  7679  cfsmolem  7780  isfin1-3  7896  axdc2lem  7958  axdc3lem4  7963  axcclem  7967  ttukeylem3  8022  gchac  8175  wunex2  8240  wuncval2  8249  inar1  8277  nn0ex  9850  xrex  10230  hashbclem  11267  ccatfn  11304  ramub1lem2  12948  prdsval  13229  imasval  13288  ipoval  14101  fpwipodrs  14111  plusffval  14214  staffval  15447  scaffval  15480  lpival  15829  psrval  15942  xrsex  16214  ipffval  16384  leordtval2  16774  1stckgen  17081  dfac14  17144  ptcmpfi  17336  hausflim  17508  flimclslem  17511  alexsubALTlem2  17574  nmfval  17943  icccmplem2  18160  tchex  18481  tchnmfval  18491  taylfval  19570  subfacp1lem3  22884  subfacp1lem5  22886  erdszelem8  22900  axlowdimlem15  23758  axlowdim  23763  basexre  24688  pgapspf  25218  isray2  25319  isray  25320  comppfsc  25473  rrnval  25717  ralxpmap  25927  elrfi  25935  istopclsd  25941  mzpcompact2lem  25995  eldioph2lem1  26005  eldioph2lem2  26006  eldioph4b  26060  diophren  26062  ttac  26295  pwslnmlem2  26361  enfixsn  26423  dfacbasgrp  26439  islindf4  26474  mendval  26657  idomsubgmo  26680  bnj918  27582  lsatset  28084  ldualset  28219  pclfinN  28993  dvaset  30098  dvhset  30175  hlhilset  31031
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108  ax-un 4403
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-rex 2514  df-v 2729  df-dif 3081  df-un 3083  df-nul 3363  df-sn 3550  df-pr 3551  df-uni 3728
  Copyright terms: Public domain W3C validator