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

Theorem uniex 4516
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 2792), 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 3836 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2349 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 4515 . . 3  |-  E. y 
y  =  U. x
54issetri 2795 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 2838 1  |-  U. A  e.  _V
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684   _Vcvv 2788   U.cuni 3827
This theorem is referenced by:  uniexg  4517  unex  4518  uniuni  4527  iunpw  4570  elxp4  5160  elxp5  5161  1stval  6124  2ndval  6125  fo1st  6139  fo2nd  6140  cnvf1o  6217  brtpos2  6240  ixpsnf1o  6856  dffi3  7184  cnfcom2  7405  cnfcom3lem  7406  cnfcom3  7407  trcl  7410  rankuni  7535  rankc2  7543  rankxpl  7547  rankxpsuc  7552  r0weon  7640  acnlem  7675  dfac3  7748  dfac5lem4  7753  dfac2a  7756  dfac8  7761  dfacacn  7767  kmlem2  7777  cfslb2n  7894  fin23lem14  7959  fin23lem16  7961  fin23lem17  7964  fin23lem38  7975  fin23lem39  7976  itunisuc  8045  axdc3lem2  8077  axcclem  8083  ac5b  8105  ttukeylem5  8140  ttukeylem6  8141  ttukey  8145  brdom7disj  8156  brdom6disj  8157  intwun  8357  wunex2  8360  wuncval2  8369  intgru  8436  pnfxr  10455  prdsval  13355  prdsds  13363  fnmrc  13509  mrcfval  13510  mrisval  13532  wunfunc  13773  wunnat  13830  arwval  13875  catcfuccl  13941  catcxpccl  13981  sylow2a  14930  zrhval  16462  distop  16733  fctop  16741  cctop  16743  ppttop  16744  epttop  16746  fncld  16759  mretopd  16829  toponmre  16830  mreclatdemo  16833  iscnp2  16969  2ndcsep  17185  kgenf  17236  ptbasin2  17273  ptbasfi  17276  dfac14  17312  alexsubALTlem2  17742  ptcmplem2  17747  ptcmplem3  17748  ptcmp  17752  minveclem4a  18794  xrge0tsmsbi  23383  esumex  23412  pwsiga  23491  sigainb  23497  dmsigagen  23505  dfrdg2  24152  trpredex  24240  fvbigcup  24442  brapply  24477  dfrdg4  24488  toplat  25290  inttop2  25515  qusp  25542  usptoplem  25546  istopx  25547  prcnt  25551  limvinlv  25559  fnessref  26293  neibastop1  26308  heiborlem1  26535  heiborlem3  26537  heibor  26545  aomclem1  27151  dfac21  27164  dicval  31366
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 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-un 4512
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-v 2790  df-uni 3828
  Copyright terms: Public domain W3C validator