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

Theorem uniex 6571
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 4246 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2529 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 6570 . . 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 1374    e. wcel 1762   _Vcvv 3106   U.cuni 4238
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-un 6567
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rex 2813  df-v 3108  df-uni 4239
This theorem is referenced by:  uniexg  6572  unex  6573  uniuni  6580  iunpw  6585  elxp4  6718  elxp5  6719  1stval  6776  2ndval  6777  fo1st  6794  fo2nd  6795  cnvf1o  6872  brtpos2  6951  ixpsnf1o  7499  dffi3  7880  cnfcom2  8135  cnfcom3lem  8136  cnfcom3  8137  cnfcom2OLD  8143  cnfcom3lemOLD  8144  cnfcom3OLD  8145  trcl  8148  rankuni  8270  rankc2  8278  rankxpl  8282  rankxpsuc  8289  r0weon  8379  acnlem  8418  dfac3  8491  dfac5lem4  8496  dfac2a  8499  dfac8  8504  dfacacn  8510  kmlem2  8520  cfslb2n  8637  fin23lem14  8702  fin23lem16  8704  fin23lem17  8707  fin23lem38  8718  fin23lem39  8719  itunisuc  8788  axdc3lem2  8820  axcclem  8826  ac5b  8847  ttukeylem5  8882  ttukeylem6  8883  ttukey  8887  brdom7disj  8898  brdom6disj  8899  intwun  9102  wunex2  9105  wuncval2  9114  intgru  9181  pnfxr  11310  prdsval  14699  prdsds  14708  fnmrc  14851  mrcfval  14852  mrisval  14874  wunfunc  15115  wunnat  15172  arwval  15217  catcfuccl  15283  catcxpccl  15323  sylow2a  16428  zrhval  18305  distop  19256  fctop  19264  cctop  19266  ppttop  19267  epttop  19269  fncld  19282  mretopd  19352  toponmre  19353  mreclatdemoBAD  19356  iscnp2  19499  2ndcsep  19719  kgenf  19770  ptbasin2  19807  ptbasfi  19810  dfac14  19847  alexsubALTlem2  20276  ptcmplem2  20281  ptcmplem3  20282  ptcmp  20286  cnextfvval  20293  cnextcn  20295  minveclem4a  21573  xrge0tsmsbi  27289  pstmfval  27361  pstmxmet  27362  esumex  27532  pwsiga  27620  sigainb  27626  dmsigagen  27634  ddemeas  27698  dfrdg2  28655  trpredex  28747  fvbigcup  28979  brapply  29015  dfrdg4  29027  ptrest  29476  mbfresfi  29489  fnessref  29616  neibastop1  29631  heiborlem1  29761  heiborlem3  29763  heibor  29771  aomclem1  30457  dfac21  30469  fourierdlem70  31296  dicval  35848
  Copyright terms: Public domain W3C validator