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

Theorem spcegv 3195
Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.)
Hypothesis
Ref Expression
spcgv.1
Assertion
Ref Expression
spcegv
Distinct variable groups:   ,   ,

Proof of Theorem spcegv
StepHypRef Expression
1 nfcv 2619 . 2
2 nfv 1707 . 2
3 spcgv.1 . 2
41, 2, 3spcegf 3190 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  E.wex 1612  e.wcel 1818
This theorem is referenced by:  spcev  3201  eqeu  3270  absneu  4104  elunii  4254  axpweq  4629  brcogw  5176  breldmg  5213  dmsnopg  5484  fvrnressn  6086  f1oexbi  6750  zfrep6  6768  unielxp  6836  ertr  7345  f1oen3g  7551  f1dom2g  7553  f1domg  7555  dom3d  7577  fodomr  7688  disjenex  7695  domssex2  7697  domssex  7698  ordiso  7962  fowdom  8018  brwdom2  8020  infeq5i  8074  oncard  8362  cardsn  8371  infxpenc2lem2  8418  infxpenc2lem2OLD  8422  dfac8b  8433  dfac8clem  8434  ac10ct  8436  ac5num  8438  acni2  8448  acnlem  8450  finnisoeu  8515  aceq3lem  8522  dfacacn  8542  infpss  8618  cflem  8647  cflecard  8654  cfslb  8667  cofsmo  8670  coftr  8674  alephsing  8677  fin4i  8699  axdc4lem  8856  ac6num  8880  axdclem2  8921  gchi  9023  grothpw  9225  hasheqf1oi  12424  fz1isolem  12510  wrd2f1tovbij  12898  climeu  13378  fsum  13542  ntrivcvgn0  13707  fprod  13748  isacs1i  15054  mreacs  15055  gsumval2a  15906  gsumval3OLD  16908  gsumval3lem2  16910  eltg3  19463  elptr  20074  uptx  20126  alexsubALTlem1  20547  ptcmplem3  20554  prdsxmslem2  21032  nbgraf1o0  24446  cusgraexg  24469  cusgrafilem3  24481  sizeusglecusg  24486  wlknwwlknbij2  24714  wlkiswwlkbij2  24721  wwlkextbij  24733  wlknwwlknvbij  24740  clwwlkbij  24799  clwwlkvbij  24801  frgrancvvdeqlem9  25041  numclwlk1lem2  25097  numclwwlk2lem3  25106  rmoeq  27386  locfinref  27844  relexpindlem  29062  wfrlem15  29357  fnimage  29579  fin2so  30040  fnessref  30175  refssfne  30176  filnetlem4  30199  unirep  30203  indexa  30224  stoweidlem5  31787  stoweidlem27  31809  stoweidlem28  31810  stoweidlem31  31813  stoweidlem43  31825  stoweidlem44  31826  stoweidlem51  31833  stoweidlem59  31841  brcici  32584  initoeu2lem2  32621  irinitoringc  32877  rp-isfinite5  37743
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-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
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-v 3111
  Copyright terms: Public domain W3C validator