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

Theorem uniex 4515
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 2793), 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 3837 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2350 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 4514 . . 3  |-  E. y 
y  =  U. x
54issetri 2796 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 2839 1  |-  U. A  e.  _V
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1685   _Vcvv 2789   U.cuni 3828
This theorem is referenced by:  uniexg  4516  unex  4517  uniuni  4526  iunpw  4569  elxp4  5158  elxp5  5159  fvex  5500  1stval  6086  2ndval  6087  fo1st  6101  fo2nd  6102  cnvf1o  6179  brtpos2  6202  ixpsnf1o  6852  dffi3  7180  cnfcom2  7401  cnfcom3lem  7402  cnfcom3  7403  trcl  7406  rankuni  7531  rankc2  7539  rankxpl  7543  rankxpsuc  7548  r0weon  7636  acnlem  7671  dfac3  7744  dfac5lem4  7749  dfac2a  7752  dfac8  7757  dfacacn  7763  kmlem2  7773  cfslb2n  7890  fin23lem14  7955  fin23lem16  7957  fin23lem17  7960  fin23lem38  7971  fin23lem39  7972  itunisuc  8041  axdc3lem2  8073  axcclem  8079  ac5b  8101  ttukeylem5  8136  ttukeylem6  8137  ttukey  8141  brdom7disj  8152  brdom6disj  8153  intwun  8353  wunex2  8356  wuncval2  8365  intgru  8432  pnfxr  10451  prdsval  13351  prdsds  13359  fnmrc  13505  mrcfval  13506  mrisval  13528  wunfunc  13769  wunnat  13826  arwval  13871  catcfuccl  13937  catcxpccl  13977  sylow2a  14926  zrhval  16458  distop  16729  fctop  16737  cctop  16739  ppttop  16740  epttop  16742  fncld  16755  mretopd  16825  toponmre  16826  mreclatdemo  16829  iscnp2  16965  2ndcsep  17181  kgenf  17232  ptbasin2  17269  ptbasfi  17272  dfac14  17308  alexsubALTlem2  17738  ptcmplem2  17743  ptcmplem3  17744  ptcmp  17748  minveclem4a  18790  dfrdg2  23556  trpredex  23644  fvbigcup  23853  brapply  23887  dfrdg4  23898  toplat  24701  inttop2  24926  qusp  24953  usptoplem  24957  istopx  24958  prcnt  24962  limvinlv  24970  fnessref  25704  neibastop1  25719  heiborlem1  25946  heiborlem3  25948  heibor  25956  aomclem1  26562  dfac21  26575  dicval  30645
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-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-rex 2550  df-v 2791  df-uni 3829
  Copyright terms: Public domain W3C validator