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

Theorem uniex 4532
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 2805), then the union of  A is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.)
Hypothesis
Ref Expression
uniex.1  |-  A  e. 
_V
Assertion
Ref Expression
uniex  |-  U. A  e.  _V

Proof of Theorem uniex
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uniex.1 . 2  |-  A  e. 
_V
2 unieq 3852 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2362 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 4531 . . 3  |-  E. y 
y  =  U. x
54issetri 2808 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 2851 1  |-  U. A  e.  _V
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696   _Vcvv 2801   U.cuni 3843
This theorem is referenced by:  uniexg  4533  unex  4534  uniuni  4543  iunpw  4586  elxp4  5176  elxp5  5177  1stval  6140  2ndval  6141  fo1st  6155  fo2nd  6156  cnvf1o  6233  brtpos2  6256  ixpsnf1o  6872  dffi3  7200  cnfcom2  7421  cnfcom3lem  7422  cnfcom3  7423  trcl  7426  rankuni  7551  rankc2  7559  rankxpl  7563  rankxpsuc  7568  r0weon  7656  acnlem  7691  dfac3  7764  dfac5lem4  7769  dfac2a  7772  dfac8  7777  dfacacn  7783  kmlem2  7793  cfslb2n  7910  fin23lem14  7975  fin23lem16  7977  fin23lem17  7980  fin23lem38  7991  fin23lem39  7992  itunisuc  8061  axdc3lem2  8093  axcclem  8099  ac5b  8121  ttukeylem5  8156  ttukeylem6  8157  ttukey  8161  brdom7disj  8172  brdom6disj  8173  intwun  8373  wunex2  8376  wuncval2  8385  intgru  8452  pnfxr  10471  prdsval  13371  prdsds  13379  fnmrc  13525  mrcfval  13526  mrisval  13548  wunfunc  13789  wunnat  13846  arwval  13891  catcfuccl  13957  catcxpccl  13997  sylow2a  14946  zrhval  16478  distop  16749  fctop  16757  cctop  16759  ppttop  16760  epttop  16762  fncld  16775  mretopd  16845  toponmre  16846  mreclatdemo  16849  iscnp2  16985  2ndcsep  17201  kgenf  17252  ptbasin2  17289  ptbasfi  17292  dfac14  17328  alexsubALTlem2  17758  ptcmplem2  17763  ptcmplem3  17764  ptcmp  17768  minveclem4a  18810  xrge0tsmsbi  23398  esumex  23427  pwsiga  23506  sigainb  23512  dmsigagen  23520  dfrdg2  24223  trpredex  24311  fvbigcup  24513  brapply  24548  dfrdg4  24560  toplat  25393  inttop2  25618  qusp  25645  usptoplem  25649  istopx  25650  prcnt  25654  limvinlv  25662  fnessref  26396  neibastop1  26411  heiborlem1  26638  heiborlem3  26640  heibor  26648  aomclem1  27254  dfac21  27267  dicval  31988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-v 2803  df-uni 3844
  Copyright terms: Public domain W3C validator