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

Theorem unex 4520
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 3843 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4219 . . 3  |-  { A ,  B }  e.  _V
54uniex 4518 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2356 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1686   _Vcvv 2790    u. cun 3152   {cpr 3643   U.cuni 3829
This theorem is referenced by:  tpex  4521  unexb  4522  fvclex  5763  unen  6945  sbthlem10  6982  unxpdomlem3  7071  isinf  7078  findcard2  7100  ac6sfi  7103  pwfilem  7152  fiin  7177  cnfcomlem  7404  trcl  7412  tc2  7429  rankxpu  7550  rankxplim  7551  rankxplim3  7553  r0weon  7642  infxpenlem  7643  dfac4  7751  dfac2  7759  kmlem2  7779  cdafn  7797  cfsmolem  7898  isfin1-3  8014  axdc2lem  8076  axdc3lem4  8081  axcclem  8085  ttukeylem3  8140  gchac  8297  wunex2  8362  wuncval2  8371  inar1  8399  nn0ex  9973  xrex  10353  hashbclem  11392  ccatfn  11429  incexclem  12297  ramub1lem2  13076  prdsval  13357  imasval  13416  ipoval  14259  fpwipodrs  14269  plusffval  14381  staffval  15614  scaffval  15647  lpival  15999  psrval  16112  xrsex  16384  ipffval  16554  leordtval2  16944  1stckgen  17251  dfac14  17314  ptcmpfi  17506  hausflim  17678  flimclslem  17681  alexsubALTlem2  17744  nmfval  18113  icccmplem2  18330  tchex  18651  tchnmfval  18661  taylfval  19740  subfacp1lem3  23715  subfacp1lem5  23717  erdszelem8  23731  axlowdimlem15  24586  axlowdim  24591  basexre  25533  pgapspf  26063  isray2  26164  isray  26165  comppfsc  26318  rrnval  26562  ralxpmap  26772  elrfi  26780  istopclsd  26786  mzpcompact2lem  26840  eldioph2lem1  26850  eldioph2lem2  26851  eldioph4b  26905  diophren  26907  ttac  27140  pwslnmlem2  27206  enfixsn  27268  dfacbasgrp  27284  islindf4  27319  mendval  27502  idomsubgmo  27525  bnj918  28869  lsatset  29253  ldualset  29388  pclfinN  30162  dvaset  31267  dvhset  31344  hlhilset  32200
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-rex 2551  df-v 2792  df-dif 3157  df-un 3159  df-nul 3458  df-sn 3648  df-pr 3649  df-uni 3830
  Copyright terms: Public domain W3C validator