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

Theorem uniex 4453
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 2744), 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
StepHypRef Expression
1 uniex.1 . 2  |-  A  e. 
_V
2 unieq 3777 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2322 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 4452 . . 3  |-  E. y 
y  =  U. x
54issetri 2747 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 2789 1  |-  U. A  e.  _V
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621   _Vcvv 2740   U.cuni 3768
This theorem is referenced by:  uniexg  4454  unex  4455  uniuni  4464  iunpw  4507  elxp4  5112  elxp5  5113  fvex  5437  1stval  6023  2ndval  6024  fo1st  6038  fo2nd  6039  cnvf1o  6116  brtpos2  6139  ixpsnf1o  6789  dffi3  7117  cnfcom2  7338  cnfcom3lem  7339  cnfcom3  7340  trcl  7343  rankuni  7468  rankc2  7476  rankxpl  7480  rankxpsuc  7485  r0weon  7573  acnlem  7608  dfac3  7681  dfac5lem4  7686  dfac2a  7689  dfac8  7694  dfacacn  7700  kmlem2  7710  cfslb2n  7827  fin23lem14  7892  fin23lem16  7894  fin23lem17  7897  fin23lem38  7908  fin23lem39  7909  itunisuc  7978  axdc3lem2  8010  axcclem  8016  ac5b  8038  ttukeylem5  8073  ttukeylem6  8074  ttukey  8078  brdom7disj  8089  brdom6disj  8090  intwun  8290  wunex2  8293  wuncval2  8302  intgru  8369  pnfxr  10387  prdsval  13282  prdsds  13290  fnmrc  13436  mrcfval  13437  mrisval  13459  wunfunc  13700  wunnat  13757  arwval  13802  catcfuccl  13868  catcxpccl  13908  sylow2a  14857  zrhval  16389  distop  16660  fctop  16668  cctop  16670  ppttop  16671  epttop  16673  fncld  16686  mretopd  16756  toponmre  16757  mreclatdemo  16760  iscnp2  16896  2ndcsep  17112  kgenf  17163  ptbasin2  17200  ptbasfi  17203  dfac14  17239  alexsubALTlem2  17669  ptcmplem2  17674  ptcmplem3  17675  ptcmp  17679  minveclem4a  18721  dfrdg2  23486  trpredex  23574  fvbigcup  23783  brapply  23817  dfrdg4  23828  toplat  24622  inttop2  24847  qusp  24874  usptoplem  24878  istopx  24879  prcnt  24883  limvinlv  24891  fnessref  25625  neibastop1  25640  heiborlem1  25867  heiborlem3  25869  heibor  25877  aomclem1  26483  dfac21  26496  dicval  30496
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 2237  ax-sep 4081  ax-un 4449
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-rex 2521  df-v 2742  df-uni 3769
  Copyright terms: Public domain W3C validator