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

Theorem unex 6377
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 4101 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4531 . . 3  |-  { A ,  B }  e.  _V
54uniex 6375 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2512 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1761   _Vcvv 2970    u. cun 3323   {cpr 3876   U.cuni 4088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-rex 2719  df-v 2972  df-dif 3328  df-un 3330  df-nul 3635  df-sn 3875  df-pr 3877  df-uni 4089
This theorem is referenced by:  tpex  6378  unexb  6379  fvclex  6548  ralxpmap  7258  unen  7388  enfixsn  7416  sbthlem10  7426  unxpdomlem3  7515  isinf  7522  findcard2  7548  ac6sfi  7552  pwfilem  7601  fiin  7668  cnfcomlem  7928  cnfcomlemOLD  7936  trcl  7944  tc2  7958  rankxpu  8079  rankxplim  8082  rankxplim3  8084  r0weon  8175  infxpenlem  8176  dfac4  8288  dfac2  8296  kmlem2  8316  cdafn  8334  cfsmolem  8435  isfin1-3  8551  axdc2lem  8613  axdc3lem4  8618  axcclem  8622  ttukeylem3  8676  gchac  8844  wunex2  8901  wuncval2  8910  inar1  8938  nn0ex  10581  xrex  10984  hashbclem  12201  ccatfn  12268  incexclem  13295  ramub1lem2  14084  prdsval  14389  imasval  14445  ipoval  15320  fpwipodrs  15330  plusffval  15423  staffval  16912  scaffval  16946  lpival  17305  psrval  17407  xrsex  17790  ipffval  18036  islindf4  18226  neitr  18743  leordtval2  18775  1stckgen  19086  dfac14  19150  ptcmpfi  19345  hausflim  19513  flimclslem  19516  alexsubALTlem2  19579  nmfval  20140  icccmplem2  20359  tchex  20691  tchnmfval  20702  taylfval  21783  legval  22970  axlowdimlem15  23137  axlowdim  23142  eengv  23160  constr3lem1  23466  constr3cyclpe  23484  3v3e3cycl2  23485  gsumle  26181  ordtconlem1  26290  sxbrsigalem2  26637  subfacp1lem3  27000  subfacp1lem5  27002  erdszelem8  27016  finixpnum  28339  comppfsc  28504  rrnval  28651  elrfi  28955  istopclsd  28961  mzpcompact2lem  29013  eldioph2lem1  29023  eldioph2lem2  29024  eldioph4b  29075  diophren  29077  ttac  29310  pwslnmlem2  29371  dfacbasgrp  29389  mendval  29465  idomsubgmo  29488  fnchoice  29676  bnj918  31593  lsatset  32357  ldualset  32492  pclfinN  33266  dvaset  34371  dvhset  34448  hlhilset  35304
  Copyright terms: Public domain W3C validator