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

Theorem uniex 6371
Description: The Axiom of Union in class notation. This says that if 
A is a set i.e.  A  e.  _V (see isset 2971), 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 4094 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
32eleq1d 2504 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
4 uniex2 6370 . . 3  |-  E. y 
y  =  U. x
54issetri 2974 . 2  |-  U. x  e.  _V
61, 3, 5vtocl 3019 1  |-  U. A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    e. wcel 1756   _Vcvv 2967   U.cuni 4086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-v 2969  df-uni 4087
This theorem is referenced by:  uniexg  6372  unex  6373  uniuni  6380  iunpw  6385  elxp4  6517  elxp5  6518  1stval  6574  2ndval  6575  fo1st  6591  fo2nd  6592  cnvf1o  6666  brtpos2  6746  ixpsnf1o  7295  dffi3  7673  cnfcom2  7927  cnfcom3lem  7928  cnfcom3  7929  cnfcom2OLD  7935  cnfcom3lemOLD  7936  cnfcom3OLD  7937  trcl  7940  rankuni  8062  rankc2  8070  rankxpl  8074  rankxpsuc  8081  r0weon  8171  acnlem  8210  dfac3  8283  dfac5lem4  8288  dfac2a  8291  dfac8  8296  dfacacn  8302  kmlem2  8312  cfslb2n  8429  fin23lem14  8494  fin23lem16  8496  fin23lem17  8499  fin23lem38  8510  fin23lem39  8511  itunisuc  8580  axdc3lem2  8612  axcclem  8618  ac5b  8639  ttukeylem5  8674  ttukeylem6  8675  ttukey  8679  brdom7disj  8690  brdom6disj  8691  intwun  8894  wunex2  8897  wuncval2  8906  intgru  8973  pnfxr  11084  prdsval  14385  prdsds  14394  fnmrc  14537  mrcfval  14538  mrisval  14560  wunfunc  14801  wunnat  14858  arwval  14903  catcfuccl  14969  catcxpccl  15009  sylow2a  16109  zrhval  17919  distop  18580  fctop  18588  cctop  18590  ppttop  18591  epttop  18593  fncld  18606  mretopd  18676  toponmre  18677  mreclatdemoBAD  18680  iscnp2  18823  2ndcsep  19043  kgenf  19094  ptbasin2  19131  ptbasfi  19134  dfac14  19171  alexsubALTlem2  19600  ptcmplem2  19605  ptcmplem3  19606  ptcmp  19610  cnextfvval  19617  cnextcn  19619  minveclem4a  20897  xrge0tsmsbi  26222  pstmfval  26292  pstmxmet  26293  esumex  26454  pwsiga  26542  sigainb  26548  dmsigagen  26556  ddemeas  26621  dfrdg2  27578  trpredex  27670  fvbigcup  27902  brapply  27938  dfrdg4  27950  ptrest  28396  mbfresfi  28409  fnessref  28536  neibastop1  28551  heiborlem1  28681  heiborlem3  28683  heibor  28691  aomclem1  29378  dfac21  29390  dicval  34714
  Copyright terms: Public domain W3C validator