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

Theorem uniex 4664
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 2920), 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 3984 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2470 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 4663 . . 3  |-  E. y 
y  =  U. x
54issetri 2923 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 2966 1  |-  U. A  e.  _V
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721   _Vcvv 2916   U.cuni 3975
This theorem is referenced by:  uniexg  4665  unex  4666  uniuni  4675  iunpw  4718  elxp4  5316  elxp5  5317  1stval  6310  2ndval  6311  fo1st  6325  fo2nd  6326  cnvf1o  6404  brtpos2  6444  ixpsnf1o  7061  dffi3  7394  cnfcom2  7615  cnfcom3lem  7616  cnfcom3  7617  trcl  7620  rankuni  7745  rankc2  7753  rankxpl  7757  rankxpsuc  7762  r0weon  7850  acnlem  7885  dfac3  7958  dfac5lem4  7963  dfac2a  7966  dfac8  7971  dfacacn  7977  kmlem2  7987  cfslb2n  8104  fin23lem14  8169  fin23lem16  8171  fin23lem17  8174  fin23lem38  8185  fin23lem39  8186  itunisuc  8255  axdc3lem2  8287  axcclem  8293  ac5b  8314  ttukeylem5  8349  ttukeylem6  8350  ttukey  8354  brdom7disj  8365  brdom6disj  8366  intwun  8566  wunex2  8569  wuncval2  8578  intgru  8645  pnfxr  10669  prdsval  13633  prdsds  13641  fnmrc  13787  mrcfval  13788  mrisval  13810  wunfunc  14051  wunnat  14108  arwval  14153  catcfuccl  14219  catcxpccl  14259  sylow2a  15208  zrhval  16744  distop  17015  fctop  17023  cctop  17025  ppttop  17026  epttop  17028  fncld  17041  mretopd  17111  toponmre  17112  mreclatdemo  17115  iscnp2  17257  2ndcsep  17475  kgenf  17526  ptbasin2  17563  ptbasfi  17566  dfac14  17603  alexsubALTlem2  18032  ptcmplem2  18037  ptcmplem3  18038  ptcmp  18042  cnextfvval  18049  cnextcn  18051  minveclem4a  19284  xrge0tsmsbi  24177  pstmfval  24244  pstmxmet  24245  esumex  24379  pwsiga  24466  sigainb  24472  dmsigagen  24480  dfrdg2  25366  trpredex  25454  fvbigcup  25656  brapply  25691  dfrdg4  25703  mbfresfi  26152  fnessref  26263  neibastop1  26278  heiborlem1  26410  heiborlem3  26412  heibor  26420  aomclem1  27019  dfac21  27032  dicval  31659
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-v 2918  df-uni 3976
  Copyright terms: Public domain W3C validator