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

Theorem uniex 6569
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 3110), 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 4243 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2523 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 6568 . . 3  |-  E. y 
y  =  U. x
54issetri 3113 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 3158 1  |-  U. A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    e. wcel 1823   _Vcvv 3106   U.cuni 4235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-v 3108  df-uni 4236
This theorem is referenced by:  uniexg  6570  unex  6571  uniuni  6582  iunpw  6587  elxp4  6717  elxp5  6718  1stval  6775  2ndval  6776  fo1st  6793  fo2nd  6794  cnvf1o  6872  brtpos2  6953  ixpsnf1o  7502  dffi3  7883  cnfcom2  8137  cnfcom3lem  8138  cnfcom3  8139  cnfcom2OLD  8145  cnfcom3lemOLD  8146  cnfcom3OLD  8147  trcl  8150  rankuni  8272  rankc2  8280  rankxpl  8284  rankxpsuc  8291  r0weon  8381  acnlem  8420  dfac3  8493  dfac5lem4  8498  dfac2a  8501  dfac8  8506  dfacacn  8512  kmlem2  8522  cfslb2n  8639  fin23lem14  8704  fin23lem16  8706  fin23lem17  8709  fin23lem38  8720  fin23lem39  8721  itunisuc  8790  axdc3lem2  8822  axcclem  8828  ac5b  8849  ttukeylem5  8884  ttukeylem6  8885  ttukey  8889  brdom7disj  8900  brdom6disj  8901  intwun  9102  wunex2  9105  wuncval2  9114  intgru  9181  pnfxr  11324  prdsval  14944  prdsds  14953  fnmrc  15096  mrcfval  15097  mrisval  15119  wunfunc  15387  wunnat  15444  arwval  15521  catcfuccl  15587  catcxpccl  15675  sylow2a  16838  zrhval  18720  distop  19664  fctop  19672  cctop  19674  ppttop  19675  epttop  19677  fncld  19690  mretopd  19760  toponmre  19761  mreclatdemoBAD  19764  iscnp2  19907  2ndcsep  20126  kgenf  20208  ptbasin2  20245  ptbasfi  20248  dfac14  20285  alexsubALTlem2  20714  ptcmplem2  20719  ptcmplem3  20720  ptcmp  20724  cnextfvval  20731  cnextcn  20733  minveclem4a  22011  xrge0tsmsbi  28011  locfinreflem  28078  pstmfval  28110  pstmxmet  28111  esumex  28258  pwsiga  28360  sigainb  28366  dmsigagen  28374  ddemeas  28445  msrval  29162  dfrdg2  29468  trpredex  29560  fvbigcup  29780  brapply  29816  dfrdg4  29828  ptrest  30288  mbfresfi  30301  fnessref  30415  neibastop1  30417  heiborlem1  30547  heiborlem3  30549  heibor  30557  aomclem1  31239  dfac21  31251  fourierdlem70  32198  dicval  37300  pwinfi  38162
  Copyright terms: Public domain W3C validator