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

Theorem spcegv 3029
Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.)
Hypothesis
Ref Expression
spcgv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
spcegv  |-  ( A  e.  V  ->  ( ps  ->  E. x ph )
)
Distinct variable groups:    ps, x    x, A
Allowed substitution hints:    ph( x)    V( x)

Proof of Theorem spcegv
StepHypRef Expression
1 nfcv 2571 . 2  |-  F/_ x A
2 nfv 1629 . 2  |-  F/ x ps
3 spcgv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3spcegf 3024 1  |-  ( A  e.  V  ->  ( ps  ->  E. x ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wex 1550    = wceq 1652    e. wcel 1725
This theorem is referenced by:  spcev  3035  eqeu  3097  absneu  3870  elunii  4012  axpweq  4368  brcogw  5033  breldmg  5067  dmsnopg  5333  zfrep6  5960  unielxp  6377  ertr  6912  f1oen3g  7115  f1dom2g  7117  f1domg  7119  dom3d  7141  fodomr  7250  disjenex  7257  domssex2  7259  domssex  7260  ordiso  7477  fowdom  7531  brwdom2  7533  infeq5i  7583  oncard  7839  cardsn  7848  infxpenc2lem2  7893  dfac8b  7904  dfac8clem  7905  ac10ct  7907  ac5num  7909  acni2  7919  acnlem  7921  finnisoeu  7986  aceq3lem  7993  dfacacn  8013  infpss  8089  cflem  8118  cflecard  8125  cfslb  8138  cofsmo  8141  coftr  8145  alephsing  8148  fin4i  8170  axdc4lem  8327  ac6num  8351  axdclem2  8392  gchi  8491  grothpw  8693  hasheqf1oi  11627  fz1isolem  11702  climeu  12341  fsum  12506  isacs1i  13874  mreacs  13875  gsumval2a  14774  gsumval3  15506  eltg3  17019  elptr  17597  uptx  17649  alexsubALTlem1  18070  ptcmplem3  18077  prdsxmslem2  18551  nbgraf1o0  21448  cusgraexg  21470  cusgrafilem3  21482  sizeusglecusg  21487  relexpindlem  25131  ntrivcvgn0  25218  fprod  25259  wfrlem15  25544  fnimage  25766  fnessref  26354  refssfne  26355  filnetlem4  26391  unirep  26395  indexa  26416  stoweidlem5  27711  stoweidlem27  27733  stoweidlem28  27734  stoweidlem31  27737  stoweidlem43  27749  stoweidlem44  27750  stoweidlem51  27757  stoweidlem59  27765  frgrancvvdeqlem9  28357
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950
  Copyright terms: Public domain W3C validator