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

Theorem uniex 4407
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 2731), 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
StepHypRef Expression
1 uniex.1 . 2  |-  A  e. 
_V
2 unieq 3736 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2319 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 4406 . . 3  |-  E. y 
y  =  U. x
54issetri 2734 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 2776 1  |-  U. A  e.  _V
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621   _Vcvv 2727   U.cuni 3727
This theorem is referenced by:  uniexg  4408  unex  4409  uniuni  4418  iunpw  4461  elxp4  5066  elxp5  5067  fvex  5391  1stval  5976  2ndval  5977  fo1st  5991  fo2nd  5992  cnvf1o  6069  brtpos2  6092  ixpsnf1o  6742  dffi3  7068  cnfcom2  7289  cnfcom3lem  7290  cnfcom3  7291  trcl  7294  rankuni  7419  rankc2  7427  rankxpl  7431  rankxpsuc  7436  r0weon  7524  acnlem  7559  dfac3  7632  dfac5lem4  7637  dfac2a  7640  dfac8  7645  dfacacn  7651  kmlem2  7661  cfslb2n  7778  fin23lem14  7843  fin23lem16  7845  fin23lem17  7848  fin23lem38  7859  fin23lem39  7860  itunisuc  7929  axdc3lem2  7961  axcclem  7967  ac5b  7989  ttukeylem5  8024  ttukeylem6  8025  ttukey  8029  brdom7disj  8040  brdom6disj  8041  intwun  8237  wunex2  8240  wuncval2  8249  intgru  8316  pnfxr  10334  prdsval  13229  prdsds  13237  fnmrc  13381  mrcfval  13382  wunfunc  13617  wunnat  13674  arwval  13719  catcfuccl  13785  catcxpccl  13825  sylow2a  14765  zrhval  16294  distop  16565  fctop  16573  cctop  16575  ppttop  16576  epttop  16578  fncld  16591  mretopd  16661  toponmre  16662  mreclatdemo  16665  iscnp2  16801  2ndcsep  17017  kgenf  17068  ptbasin2  17105  ptbasfi  17108  dfac14  17144  alexsubALTlem2  17574  ptcmplem2  17579  ptcmplem3  17580  ptcmp  17584  minveclem4a  18626  dfrdg2  23320  trpredex  23408  fvbigcup  23617  brapply  23651  dfrdg4  23662  toplat  24456  inttop2  24681  qusp  24708  usptoplem  24712  istopx  24713  prcnt  24717  limvinlv  24725  fnessref  25459  neibastop1  25474  heiborlem1  25701  heiborlem3  25703  heibor  25711  aomclem1  26317  dfac21  26330  dicval  30055
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-un 4403
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-rex 2514  df-v 2729  df-uni 3728
  Copyright terms: Public domain W3C validator