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

Theorem uniexg 6597
Description: The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent instead of to make the theorem more general and thus shorten some proofs; obviously the universal class constant is one possible substitution for class variable . (Contributed by NM, 25-Nov-1994.)
Assertion
Ref Expression
uniexg

Proof of Theorem uniexg
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 unieq 4257 . . 3
21eleq1d 2526 . 2
3 vex 3112 . . 3
43uniex 6596 . 2
52, 4vtoclg 3167 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818   cvv 3109  U.cuni 4249
This theorem is referenced by:  snnex  6606  uniexb  6610  ssonuni  6622  ssonprc  6627  dmexg  6731  rnexg  6732  iunexg  6776  undefval  7024  onovuni  7032  tz7.44lem1  7090  tz7.44-3  7093  en1b  7603  en1uniel  7607  disjen  7694  domss2  7696  fival  7892  fipwuni  7906  supexd  7933  cantnflem1  8129  cantnflem1OLD  8152  dfac8clem  8434  onssnum  8442  dfac12lem1  8544  dfac12lem2  8545  fin1a2lem12  8812  hsmexlem1  8827  axdc2lem  8849  ttukeylem3  8912  wrdexb  12558  restid  14831  prdsbas  14854  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  prdshom  14864  sscpwex  15184  pmtrfv  16477  frgpcyg  18612  eltopspOLD  19419  istpsOLD  19421  istopon  19426  tgval  19456  eltg  19458  eltg2  19459  tgss2  19489  ntrval  19537  neiptoptop  19632  neiptopnei  19633  restin  19667  neitr  19681  restntr  19683  cnpresti  19789  cnprest  19790  cnprest2  19791  lmcnp  19805  pnrmopn  19844  cnrmnrm  19862  cmpsublem  19899  cmpsub  19900  cmpcld  19902  bwthOLD  19911  hausmapdom  20001  isref  20010  locfindis  20031  txbasex  20067  dfac14lem  20118  uptx  20126  xkopt  20156  xkopjcn  20157  qtopval2  20197  elqtop  20198  fbssfi  20338  ptcmplem2  20553  cnextfval  20562  cnextcn  20567  tuslem  20770  isppw  23388  hasheuni  28091  insiga  28137  sigagenval  28140  braew  28214  omsval  28264  sibfof  28282  isrrvv  28382  rrvmulc  28392  kur14  28660  cvmscld  28718  relexp0  29052  relexpsucr  29053  nobndlem1  29452  fobigcup  29550  hfuni  29841  mbfresfi  30061  isfne  30157  isfne4b  30159  topjoin  30183  fnemeet1  30184  tailfval  30190  supex2g  30228  kelac2  31011  cnfex  31403  stoweidlem50  31832  stoweidlem57  31839  stoweidlem59  31841  stoweidlem60  31842  fourierdlem71  31960  bnj1489  34112
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