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

Theorem uniex 6476
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 3072), 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 4197 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2520 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 6475 . . 3  |-  E. y 
y  =  U. x
54issetri 3075 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 3120 1  |-  U. A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    e. wcel 1758   _Vcvv 3068   U.cuni 4189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-un 6472
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rex 2801  df-v 3070  df-uni 4190
This theorem is referenced by:  uniexg  6477  unex  6478  uniuni  6485  iunpw  6490  elxp4  6622  elxp5  6623  1stval  6679  2ndval  6680  fo1st  6696  fo2nd  6697  cnvf1o  6771  brtpos2  6851  ixpsnf1o  7403  dffi3  7782  cnfcom2  8036  cnfcom3lem  8037  cnfcom3  8038  cnfcom2OLD  8044  cnfcom3lemOLD  8045  cnfcom3OLD  8046  trcl  8049  rankuni  8171  rankc2  8179  rankxpl  8183  rankxpsuc  8190  r0weon  8280  acnlem  8319  dfac3  8392  dfac5lem4  8397  dfac2a  8400  dfac8  8405  dfacacn  8411  kmlem2  8421  cfslb2n  8538  fin23lem14  8603  fin23lem16  8605  fin23lem17  8608  fin23lem38  8619  fin23lem39  8620  itunisuc  8689  axdc3lem2  8721  axcclem  8727  ac5b  8748  ttukeylem5  8783  ttukeylem6  8784  ttukey  8788  brdom7disj  8799  brdom6disj  8800  intwun  9003  wunex2  9006  wuncval2  9015  intgru  9082  pnfxr  11193  prdsval  14495  prdsds  14504  fnmrc  14647  mrcfval  14648  mrisval  14670  wunfunc  14911  wunnat  14968  arwval  15013  catcfuccl  15079  catcxpccl  15119  sylow2a  16222  zrhval  18048  distop  18716  fctop  18724  cctop  18726  ppttop  18727  epttop  18729  fncld  18742  mretopd  18812  toponmre  18813  mreclatdemoBAD  18816  iscnp2  18959  2ndcsep  19179  kgenf  19230  ptbasin2  19267  ptbasfi  19270  dfac14  19307  alexsubALTlem2  19736  ptcmplem2  19741  ptcmplem3  19742  ptcmp  19746  cnextfvval  19753  cnextcn  19755  minveclem4a  21033  xrge0tsmsbi  26388  pstmfval  26457  pstmxmet  26458  esumex  26619  pwsiga  26707  sigainb  26713  dmsigagen  26721  ddemeas  26786  dfrdg2  27743  trpredex  27835  fvbigcup  28067  brapply  28103  dfrdg4  28115  ptrest  28563  mbfresfi  28576  fnessref  28703  neibastop1  28718  heiborlem1  28848  heiborlem3  28850  heibor  28858  aomclem1  29545  dfac21  29557  dicval  35127
  Copyright terms: Public domain W3C validator