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

Theorem uniex 4518
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 2794), 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 3838 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2351 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 4517 . . 3  |-  E. y 
y  =  U. x
54issetri 2797 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 2840 1  |-  U. A  e.  _V
Colors of variables: wff set class
Syntax hints:    = wceq 1625    e. wcel 1686   _Vcvv 2790   U.cuni 3829
This theorem is referenced by:  uniexg  4519  unex  4520  uniuni  4529  iunpw  4572  elxp4  5162  elxp5  5163  1stval  6126  2ndval  6127  fo1st  6141  fo2nd  6142  cnvf1o  6219  brtpos2  6242  ixpsnf1o  6858  dffi3  7186  cnfcom2  7407  cnfcom3lem  7408  cnfcom3  7409  trcl  7412  rankuni  7537  rankc2  7545  rankxpl  7549  rankxpsuc  7554  r0weon  7642  acnlem  7677  dfac3  7750  dfac5lem4  7755  dfac2a  7758  dfac8  7763  dfacacn  7769  kmlem2  7779  cfslb2n  7896  fin23lem14  7961  fin23lem16  7963  fin23lem17  7966  fin23lem38  7977  fin23lem39  7978  itunisuc  8047  axdc3lem2  8079  axcclem  8085  ac5b  8107  ttukeylem5  8142  ttukeylem6  8143  ttukey  8147  brdom7disj  8158  brdom6disj  8159  intwun  8359  wunex2  8362  wuncval2  8371  intgru  8438  pnfxr  10457  prdsval  13357  prdsds  13365  fnmrc  13511  mrcfval  13512  mrisval  13534  wunfunc  13775  wunnat  13832  arwval  13877  catcfuccl  13943  catcxpccl  13983  sylow2a  14932  zrhval  16464  distop  16735  fctop  16743  cctop  16745  ppttop  16746  epttop  16748  fncld  16761  mretopd  16831  toponmre  16832  mreclatdemo  16835  iscnp2  16971  2ndcsep  17187  kgenf  17238  ptbasin2  17275  ptbasfi  17278  dfac14  17314  alexsubALTlem2  17744  ptcmplem2  17749  ptcmplem3  17750  ptcmp  17754  minveclem4a  18796  xrge0tsmsbi  23385  esumex  23414  pwsiga  23493  sigainb  23499  dmsigagen  23507  dfrdg2  24154  trpredex  24242  fvbigcup  24444  brapply  24479  dfrdg4  24490  toplat  25301  inttop2  25526  qusp  25553  usptoplem  25557  istopx  25558  prcnt  25562  limvinlv  25570  fnessref  26304  neibastop1  26319  heiborlem1  26546  heiborlem3  26548  heibor  26556  aomclem1  27162  dfac21  27175  dicval  31439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rex 2551  df-v 2792  df-uni 3830
  Copyright terms: Public domain W3C validator