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

Theorem unex 6497
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 4176 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4604 . . 3  |-  { A ,  B }  e.  _V
54uniex 6495 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2467 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1826   _Vcvv 3034    u. cun 3387   {cpr 3946   U.cuni 4163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601  ax-un 6491
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-rex 2738  df-v 3036  df-dif 3392  df-un 3394  df-nul 3712  df-sn 3945  df-pr 3947  df-uni 4164
This theorem is referenced by:  tpex  6498  unexb  6499  fvclex  6671  ralxpmap  7387  unen  7517  enfixsn  7545  sbthlem10  7555  unxpdomlem3  7642  isinf  7649  findcard2  7675  ac6sfi  7679  pwfilem  7729  fiin  7797  cnfcomlem  8056  cnfcomlemOLD  8064  trcl  8072  tc2  8086  rankxpu  8207  rankxplim  8210  rankxplim3  8212  r0weon  8303  infxpenlem  8304  dfac4  8416  dfac2  8424  kmlem2  8444  cdafn  8462  cfsmolem  8563  isfin1-3  8679  axdc2lem  8741  axdc3lem4  8746  axcclem  8750  ttukeylem3  8804  gchac  8970  wunex2  9027  wuncval2  9036  inar1  9064  nn0ex  10718  xrex  11136  hashbclem  12405  ccatfnOLD  12500  incexclem  13650  ramub1lem2  14547  prdsval  14862  imasval  14918  ipoval  15901  fpwipodrs  15911  plusffval  15994  staffval  17609  scaffval  17643  lpival  18006  psrval  18124  xrsex  18546  ipffval  18774  islindf4  18958  neitr  19767  leordtval2  19799  comppfsc  20118  1stckgen  20140  dfac14  20204  ptcmpfi  20399  hausflim  20567  flimclslem  20570  alexsubALTlem2  20633  nmfval  21194  icccmplem2  21413  tchex  21745  tchnmfval  21756  taylfval  22839  legval  24091  axlowdimlem15  24380  axlowdim  24385  eengv  24403  constr3lem1  24766  constr3cyclpe  24784  3v3e3cycl2  24785  padct  27695  ordtconlem1  28060  sxbrsigalem2  28413  subfacp1lem3  28815  subfacp1lem5  28817  erdszelem8  28831  mrexval  29050  mrsubcv  29059  mrsubff  29061  mrsubccat  29067  elmrsubrn  29069  finixpnum  30203  rrnval  30489  elrfi  30792  istopclsd  30798  mzpcompact2lem  30849  eldioph2lem1  30858  eldioph2lem2  30859  eldioph4b  30910  diophren  30912  ttac  31144  pwslnmlem2  31205  dfacbasgrp  31225  mendval  31300  idomsubgmo  31323  fnchoice  31571  limcresiooub  31814  limcresioolb  31815  fourierdlem48  32103  fourierdlem49  32104  fourierdlem102  32157  fourierdlem114  32169  bnj918  34171  lsatset  35128  ldualset  35263  pclfinN  36037  dvaset  37144  dvhset  37221  hlhilset  38077  superuncl  38182  ssuncl  38184  sssymdifcl  38186  dfrcl2  38211  comptiunov2i  38234  cotrclrcl  38250  frege83  38445  frege110  38472  frege133  38495
  Copyright terms: Public domain W3C validator