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

Theorem uniex 6596
 Description: The Axiom of Union in class notation. This says that if is a set i.e. (see isset 3113), then the union of is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.)
Hypothesis
Ref Expression
uniex.1
Assertion
Ref Expression
uniex

Proof of Theorem uniex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uniex.1 . 2
2 unieq 4257 . . 3
32eleq1d 2526 . 2
4 uniex2 6595 . . 3
54issetri 3116 . 2
61, 3, 5vtocl 3161 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395  e.wcel 1818   cvv 3109  U.cuni 4249 This theorem is referenced by:  uniexg  6597  unex  6598  uniuni  6609  iunpw  6614  elxp4  6744  elxp5  6745  1stval  6802  2ndval  6803  fo1st  6820  fo2nd  6821  cnvf1o  6899  brtpos2  6980  ixpsnf1o  7529  dffi3  7911  cnfcom2  8167  cnfcom3lem  8168  cnfcom3  8169  cnfcom2OLD  8175  cnfcom3lemOLD  8176  cnfcom3OLD  8177  trcl  8180  rankuni  8302  rankc2  8310  rankxpl  8314  rankxpsuc  8321  r0weon  8411  acnlem  8450  dfac3  8523  dfac5lem4  8528  dfac2a  8531  dfac8  8536  dfacacn  8542  kmlem2  8552  cfslb2n  8669  fin23lem14  8734  fin23lem16  8736  fin23lem17  8739  fin23lem38  8750  fin23lem39  8751  itunisuc  8820  axdc3lem2  8852  axcclem  8858  ac5b  8879  ttukeylem5  8914  ttukeylem6  8915  ttukey  8919  brdom7disj  8930  brdom6disj  8931  intwun  9134  wunex2  9137  wuncval2  9146  intgru  9213  pnfxr  11350  prdsval  14852  prdsds  14861  fnmrc  15004  mrcfval  15005  mrisval  15027  wunfunc  15268  wunnat  15325  arwval  15370  catcfuccl  15436  catcxpccl  15476  sylow2a  16639  zrhval  18545  distop  19497  fctop  19505  cctop  19507  ppttop  19508  epttop  19510  fncld  19523  mretopd  19593  toponmre  19594  mreclatdemoBAD  19597  iscnp2  19740  2ndcsep  19960  kgenf  20042  ptbasin2  20079  ptbasfi  20082  dfac14  20119  alexsubALTlem2  20548  ptcmplem2  20553  ptcmplem3  20554  ptcmp  20558  cnextfvval  20565  cnextcn  20567  minveclem4a  21845  xrge0tsmsbi  27776  locfinreflem  27843  pstmfval  27875  pstmxmet  27876  esumex  28042  pwsiga  28130  sigainb  28136  dmsigagen  28144  ddemeas  28208  msrval  28898  dfrdg2  29228  trpredex  29320  fvbigcup  29552  brapply  29588  dfrdg4  29600  ptrest  30048  mbfresfi  30061  fnessref  30175  neibastop1  30177  heiborlem1  30307  heiborlem3  30309  heibor  30317  aomclem1  31000  dfac21  31012  fourierdlem70  31959  dicval  36903  pwinfi  37749 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-un 6592 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-v 3111  df-uni 4250
 Copyright terms: Public domain W3C validator