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

Theorem uniex 4619
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 2877), 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 3938 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2432 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 4618 . . 3  |-  E. y 
y  =  U. x
54issetri 2880 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 2923 1  |-  U. A  e.  _V
Colors of variables: wff set class
Syntax hints:    = wceq 1647    e. wcel 1715   _Vcvv 2873   U.cuni 3929
This theorem is referenced by:  uniexg  4620  unex  4621  uniuni  4630  iunpw  4673  elxp4  5263  elxp5  5264  1stval  6251  2ndval  6252  fo1st  6266  fo2nd  6267  cnvf1o  6345  brtpos2  6382  ixpsnf1o  6999  dffi3  7331  cnfcom2  7552  cnfcom3lem  7553  cnfcom3  7554  trcl  7557  rankuni  7682  rankc2  7690  rankxpl  7694  rankxpsuc  7699  r0weon  7787  acnlem  7822  dfac3  7895  dfac5lem4  7900  dfac2a  7903  dfac8  7908  dfacacn  7914  kmlem2  7924  cfslb2n  8041  fin23lem14  8106  fin23lem16  8108  fin23lem17  8111  fin23lem38  8122  fin23lem39  8123  itunisuc  8192  axdc3lem2  8224  axcclem  8230  ac5b  8252  ttukeylem5  8287  ttukeylem6  8288  ttukey  8292  brdom7disj  8303  brdom6disj  8304  intwun  8504  wunex2  8507  wuncval2  8516  intgru  8583  pnfxr  10606  prdsval  13565  prdsds  13573  fnmrc  13719  mrcfval  13720  mrisval  13742  wunfunc  13983  wunnat  14040  arwval  14085  catcfuccl  14151  catcxpccl  14191  sylow2a  15140  zrhval  16679  distop  16950  fctop  16958  cctop  16960  ppttop  16961  epttop  16963  fncld  16976  mretopd  17046  toponmre  17047  mreclatdemo  17050  iscnp2  17186  2ndcsep  17402  kgenf  17453  ptbasin2  17490  ptbasfi  17493  dfac14  17529  alexsubALTlem2  17955  ptcmplem2  17960  ptcmplem3  17961  ptcmp  17965  minveclem4a  19009  xrge0tsmsbi  23736  cnextfvval  23822  cnextcn  23824  esumex  24012  pwsiga  24099  sigainb  24105  dmsigagen  24113  dfrdg2  24978  trpredex  25066  fvbigcup  25268  brapply  25303  dfrdg4  25315  fnessref  25885  neibastop1  25900  heiborlem1  26126  heiborlem3  26128  heibor  26136  aomclem1  26742  dfac21  26755  dicval  31425
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-un 4615
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rex 2634  df-v 2875  df-uni 3930
  Copyright terms: Public domain W3C validator