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

Theorem spcegv 2869
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 2419 . 2  |-  F/_ x A
2 nfv 1605 . 2  |-  F/ x ps
3 spcgv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3spcegf 2864 1  |-  ( A  e.  V  ->  ( ps  ->  E. x ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wex 1528    = wceq 1623    e. wcel 1684
This theorem is referenced by:  spcev  2875  eqeu  2936  absneu  3701  elunii  3832  axpweq  4187  breldmg  4884  dmsnopg  5144  zfrep6  5748  unielxp  6158  ertr  6675  f1oen3g  6877  f1dom2g  6879  f1domg  6881  dom3d  6903  fodomr  7012  disjenex  7019  domssex2  7021  domssex  7022  ordiso  7231  fowdom  7285  brwdom2  7287  infeq5i  7337  oncard  7593  cardsn  7602  infxpenc2lem2  7647  dfac8b  7658  dfac8clem  7659  ac10ct  7661  ac5num  7663  acni2  7673  acnlem  7675  finnisoeu  7740  aceq3lem  7747  dfacacn  7767  infpss  7843  cflem  7872  cflecard  7879  cfslb  7892  cofsmo  7895  coftr  7899  alephsing  7902  fin4i  7924  axdc4lem  8081  ac6num  8106  axdclem2  8147  gchi  8246  grothpw  8448  fz1isolem  11399  climeu  12029  fsum  12193  isacs1i  13559  mreacs  13560  gsumval2a  14459  gsumval3  15191  eltg3  16700  elptr  17268  uptx  17319  alexsubALTlem1  17741  ptcmplem3  17748  prdsxmslem2  18075  relexpindlem  23447  wfrlem15  23681  fnimage  23879  funpartfv  23894  injrec2  24531  prl  24579  dffprod  24731  indcls2  25408  fnessref  25705  refssfne  25706  filnetlem4  25742  unirep  25761  indexa  25824  fnchoice  27112  stoweidlem5  27166  stoweidlem27  27188  stoweidlem28  27189  stoweidlem31  27192  stoweidlem43  27204  stoweidlem44  27205  stoweidlem51  27212  stoweidlem59  27220
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790
  Copyright terms: Public domain W3C validator