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

Theorem uniex 6365
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 2966), 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 4087 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2499 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 6364 . . 3  |-  E. y 
y  =  U. x
54issetri 2969 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 3013 1  |-  U. A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362    e. wcel 1755   _Vcvv 2962   U.cuni 4079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-v 2964  df-uni 4080
This theorem is referenced by:  uniexg  6366  unex  6367  uniuni  6374  iunpw  6379  elxp4  6511  elxp5  6512  1stval  6568  2ndval  6569  fo1st  6585  fo2nd  6586  cnvf1o  6660  brtpos2  6740  ixpsnf1o  7291  dffi3  7669  cnfcom2  7923  cnfcom3lem  7924  cnfcom3  7925  cnfcom2OLD  7931  cnfcom3lemOLD  7932  cnfcom3OLD  7933  trcl  7936  rankuni  8058  rankc2  8066  rankxpl  8070  rankxpsuc  8077  r0weon  8167  acnlem  8206  dfac3  8279  dfac5lem4  8284  dfac2a  8287  dfac8  8292  dfacacn  8298  kmlem2  8308  cfslb2n  8425  fin23lem14  8490  fin23lem16  8492  fin23lem17  8495  fin23lem38  8506  fin23lem39  8507  itunisuc  8576  axdc3lem2  8608  axcclem  8614  ac5b  8635  ttukeylem5  8670  ttukeylem6  8671  ttukey  8675  brdom7disj  8686  brdom6disj  8687  intwun  8890  wunex2  8893  wuncval2  8902  intgru  8969  pnfxr  11080  prdsval  14376  prdsds  14385  fnmrc  14528  mrcfval  14529  mrisval  14551  wunfunc  14792  wunnat  14849  arwval  14894  catcfuccl  14960  catcxpccl  15000  sylow2a  16098  zrhval  17781  distop  18442  fctop  18450  cctop  18452  ppttop  18453  epttop  18455  fncld  18468  mretopd  18538  toponmre  18539  mreclatdemoBAD  18542  iscnp2  18685  2ndcsep  18905  kgenf  18956  ptbasin2  18993  ptbasfi  18996  dfac14  19033  alexsubALTlem2  19462  ptcmplem2  19467  ptcmplem3  19468  ptcmp  19472  cnextfvval  19479  cnextcn  19481  minveclem4a  20759  xrge0tsmsbi  26107  pstmfval  26177  pstmxmet  26178  esumex  26339  pwsiga  26427  sigainb  26433  dmsigagen  26441  ddemeas  26506  dfrdg2  27456  trpredex  27548  fvbigcup  27780  brapply  27816  dfrdg4  27828  ptrest  28269  mbfresfi  28282  fnessref  28409  neibastop1  28424  heiborlem1  28554  heiborlem3  28556  heibor  28564  aomclem1  29252  dfac21  29264  dicval  34394
  Copyright terms: Public domain W3C validator