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

Theorem unex 4517
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 3842 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4216 . . 3  |-  { A ,  B }  e.  _V
54uniex 4515 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2355 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1685   _Vcvv 2789    u. cun 3151   {cpr 3642   U.cuni 3828
This theorem is referenced by:  tpex  4518  unexb  4519  fvclex  5723  unen  6939  sbthlem10  6976  unxpdomlem3  7065  isinf  7072  findcard2  7094  ac6sfi  7097  pwfilem  7146  fiin  7171  cnfcomlem  7398  trcl  7406  tc2  7423  rankxpu  7544  rankxplim  7545  rankxplim3  7547  r0weon  7636  infxpenlem  7637  dfac4  7745  dfac2  7753  kmlem2  7773  cdafn  7791  cfsmolem  7892  isfin1-3  8008  axdc2lem  8070  axdc3lem4  8075  axcclem  8079  ttukeylem3  8134  gchac  8291  wunex2  8356  wuncval2  8365  inar1  8393  nn0ex  9967  xrex  10347  hashbclem  11386  ccatfn  11423  incexclem  12291  ramub1lem2  13070  prdsval  13351  imasval  13410  ipoval  14253  fpwipodrs  14263  plusffval  14375  staffval  15608  scaffval  15641  lpival  15993  psrval  16106  xrsex  16378  ipffval  16548  leordtval2  16938  1stckgen  17245  dfac14  17308  ptcmpfi  17500  hausflim  17672  flimclslem  17675  alexsubALTlem2  17738  nmfval  18107  icccmplem2  18324  tchex  18645  tchnmfval  18655  taylfval  19734  subfacp1lem3  23120  subfacp1lem5  23122  erdszelem8  23136  axlowdimlem15  23994  axlowdim  23999  basexre  24933  pgapspf  25463  isray2  25564  isray  25565  comppfsc  25718  rrnval  25962  ralxpmap  26172  elrfi  26180  istopclsd  26186  mzpcompact2lem  26240  eldioph2lem1  26250  eldioph2lem2  26251  eldioph4b  26305  diophren  26307  ttac  26540  pwslnmlem2  26606  enfixsn  26668  dfacbasgrp  26684  islindf4  26719  mendval  26902  idomsubgmo  26925  bnj918  28075  lsatset  28459  ldualset  28594  pclfinN  29368  dvaset  30473  dvhset  30550  hlhilset  31406
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-rex 2550  df-v 2791  df-dif 3156  df-un 3158  df-nul 3457  df-sn 3647  df-pr 3648  df-uni 3829
  Copyright terms: Public domain W3C validator