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

Theorem unex 6583
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 4247 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4679 . . 3  |-  { A ,  B }  e.  _V
54uniex 6581 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2528 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1804   _Vcvv 3095    u. cun 3459   {cpr 4016   U.cuni 4234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-rex 2799  df-v 3097  df-dif 3464  df-un 3466  df-nul 3771  df-sn 4015  df-pr 4017  df-uni 4235
This theorem is referenced by:  tpex  6584  unexb  6585  fvclex  6757  ralxpmap  7470  unen  7600  enfixsn  7628  sbthlem10  7638  unxpdomlem3  7728  isinf  7735  findcard2  7762  ac6sfi  7766  pwfilem  7816  fiin  7884  cnfcomlem  8146  cnfcomlemOLD  8154  trcl  8162  tc2  8176  rankxpu  8297  rankxplim  8300  rankxplim3  8302  r0weon  8393  infxpenlem  8394  dfac4  8506  dfac2  8514  kmlem2  8534  cdafn  8552  cfsmolem  8653  isfin1-3  8769  axdc2lem  8831  axdc3lem4  8836  axcclem  8840  ttukeylem3  8894  gchac  9062  wunex2  9119  wuncval2  9128  inar1  9156  nn0ex  10808  xrex  11228  hashbclem  12483  ccatfn  12573  incexclem  13630  ramub1lem2  14527  prdsval  14834  imasval  14890  ipoval  15763  fpwipodrs  15773  plusffval  15856  staffval  17475  scaffval  17509  lpival  17872  psrval  17990  xrsex  18412  ipffval  18661  islindf4  18851  neitr  19659  leordtval2  19691  comppfsc  20011  1stckgen  20033  dfac14  20097  ptcmpfi  20292  hausflim  20460  flimclslem  20463  alexsubALTlem2  20526  nmfval  21087  icccmplem2  21306  tchex  21638  tchnmfval  21649  taylfval  22732  legval  23949  axlowdimlem15  24237  axlowdim  24242  eengv  24260  constr3lem1  24623  constr3cyclpe  24641  3v3e3cycl2  24642  ordtconlem1  27884  sxbrsigalem2  28235  subfacp1lem3  28604  subfacp1lem5  28606  erdszelem8  28620  mrexval  28839  mrsubcv  28848  mrsubff  28850  mrsubccat  28856  elmrsubrn  28858  finixpnum  30014  rrnval  30299  elrfi  30602  istopclsd  30608  mzpcompact2lem  30660  eldioph2lem1  30669  eldioph2lem2  30670  eldioph4b  30721  diophren  30723  ttac  30954  pwslnmlem2  31015  dfacbasgrp  31033  mendval  31108  idomsubgmo  31131  fnchoice  31358  limcresiooub  31602  limcresioolb  31603  fourierdlem48  31891  fourierdlem49  31892  fourierdlem102  31945  fourierdlem114  31957  bnj918  33692  lsatset  34590  ldualset  34725  pclfinN  35499  dvaset  36606  dvhset  36683  hlhilset  37539  superuncl  37591  ssuncl  37593  sssymdifcl  37595  trclubg  37613
  Copyright terms: Public domain W3C validator