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

Theorem unex 4490
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 3815 . 2  |-  U. { A ,  B }  =  ( A  u.  B )
4 prex 4189 . . 3  |-  { A ,  B }  e.  _V
54uniex 4488 . 2  |-  U. { A ,  B }  e.  _V
63, 5eqeltrri 2329 1  |-  ( A  u.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2763    u. cun 3125   {cpr 3615   U.cuni 3801
This theorem is referenced by:  tpex  4491  unexb  4492  fvclex  5695  unen  6911  sbthlem10  6948  unxpdomlem3  7037  isinf  7044  findcard2  7066  ac6sfi  7069  pwfilem  7118  fiin  7143  cnfcomlem  7370  trcl  7378  tc2  7395  rankxpu  7516  rankxplim  7517  rankxplim3  7519  r0weon  7608  infxpenlem  7609  dfac4  7717  dfac2  7725  kmlem2  7745  cdafn  7763  cfsmolem  7864  isfin1-3  7980  axdc2lem  8042  axdc3lem4  8047  axcclem  8051  ttukeylem3  8106  gchac  8263  wunex2  8328  wuncval2  8337  inar1  8365  nn0ex  9939  xrex  10319  hashbclem  11356  ccatfn  11393  ramub1lem2  13037  prdsval  13318  imasval  13377  ipoval  14220  fpwipodrs  14230  plusffval  14342  staffval  15575  scaffval  15608  lpival  15960  psrval  16073  xrsex  16345  ipffval  16515  leordtval2  16905  1stckgen  17212  dfac14  17275  ptcmpfi  17467  hausflim  17639  flimclslem  17642  alexsubALTlem2  17705  nmfval  18074  icccmplem2  18291  tchex  18612  tchnmfval  18622  taylfval  19701  subfacp1lem3  23086  subfacp1lem5  23088  erdszelem8  23102  axlowdimlem15  23960  axlowdim  23965  basexre  24890  pgapspf  25420  isray2  25521  isray  25522  comppfsc  25675  rrnval  25919  ralxpmap  26129  elrfi  26137  istopclsd  26143  mzpcompact2lem  26197  eldioph2lem1  26207  eldioph2lem2  26208  eldioph4b  26262  diophren  26264  ttac  26497  pwslnmlem2  26563  enfixsn  26625  dfacbasgrp  26641  islindf4  26676  mendval  26859  idomsubgmo  26882  bnj918  27928  lsatset  28430  ldualset  28565  pclfinN  29339  dvaset  30444  dvhset  30521  hlhilset  31377
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186  ax-un 4484
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-rex 2524  df-v 2765  df-dif 3130  df-un 3132  df-nul 3431  df-sn 3620  df-pr 3621  df-uni 3802
  Copyright terms: Public domain W3C validator