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

Theorem unex 4640
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 3964 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4340 . . 3  |-  { A ,  B }  e.  _V
54uniex 4638 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2451 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   _Vcvv 2892    u. cun 3254   {cpr 3751   U.cuni 3950
This theorem is referenced by:  tpex  4641  unexb  4642  fvclex  5913  unen  7118  sbthlem10  7155  unxpdomlem3  7244  isinf  7251  findcard2  7277  ac6sfi  7280  pwfilem  7329  fiin  7355  cnfcomlem  7582  trcl  7590  tc2  7607  rankxpu  7728  rankxplim  7729  rankxplim3  7731  r0weon  7820  infxpenlem  7821  dfac4  7929  dfac2  7937  kmlem2  7957  cdafn  7975  cfsmolem  8076  isfin1-3  8192  axdc2lem  8254  axdc3lem4  8259  axcclem  8263  ttukeylem3  8317  gchac  8474  wunex2  8539  wuncval2  8548  inar1  8576  nn0ex  10152  xrex  10534  hashbclem  11621  ccatfn  11661  incexclem  12536  ramub1lem2  13315  prdsval  13598  imasval  13657  ipoval  14500  fpwipodrs  14510  plusffval  14622  staffval  15855  scaffval  15888  lpival  16236  psrval  16349  xrsex  16632  ipffval  16795  neitr  17159  leordtval2  17191  1stckgen  17500  dfac14  17564  ptcmpfi  17759  hausflim  17927  flimclslem  17930  alexsubALTlem2  17993  nmfval  18500  icccmplem2  18718  tchex  19040  tchnmfval  19050  taylfval  20135  constr3lem1  21473  constr3cyclpe  21491  3v3e3cycl2  21492  sxbrsigalem2  24423  subfacp1lem3  24640  subfacp1lem5  24642  erdszelem8  24656  axlowdimlem15  25602  axlowdim  25607  comppfsc  26071  rrnval  26220  ralxpmap  26426  elrfi  26432  istopclsd  26438  mzpcompact2lem  26492  eldioph2lem1  26502  eldioph2lem2  26503  eldioph4b  26556  diophren  26558  ttac  26791  pwslnmlem2  26857  enfixsn  26919  dfacbasgrp  26935  islindf4  26970  mendval  27153  idomsubgmo  27176  fnchoice  27361  bnj918  28466  lsatset  29156  ldualset  29291  pclfinN  30065  dvaset  31170  dvhset  31247  hlhilset  32103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-nul 4272  ax-pr 4337  ax-un 4634
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-rex 2648  df-v 2894  df-dif 3259  df-un 3261  df-nul 3565  df-sn 3756  df-pr 3757  df-uni 3951
  Copyright terms: Public domain W3C validator