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

Theorem spcegv 2882
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 2432 . 2  |-  F/_ x A
2 nfv 1609 . 2  |-  F/ x ps
3 spcgv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3spcegf 2877 1  |-  ( A  e.  V  ->  ( ps  ->  E. x ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wex 1531    = wceq 1632    e. wcel 1696
This theorem is referenced by:  spcev  2888  eqeu  2949  absneu  3714  elunii  3848  axpweq  4203  breldmg  4900  dmsnopg  5160  zfrep6  5764  unielxp  6174  ertr  6691  f1oen3g  6893  f1dom2g  6895  f1domg  6897  dom3d  6919  fodomr  7028  disjenex  7035  domssex2  7037  domssex  7038  ordiso  7247  fowdom  7301  brwdom2  7303  infeq5i  7353  oncard  7609  cardsn  7618  infxpenc2lem2  7663  dfac8b  7674  dfac8clem  7675  ac10ct  7677  ac5num  7679  acni2  7689  acnlem  7691  finnisoeu  7756  aceq3lem  7763  dfacacn  7783  infpss  7859  cflem  7888  cflecard  7895  cfslb  7908  cofsmo  7911  coftr  7915  alephsing  7918  fin4i  7940  axdc4lem  8097  ac6num  8122  axdclem2  8163  gchi  8262  grothpw  8464  fz1isolem  11415  climeu  12045  fsum  12209  isacs1i  13575  mreacs  13576  gsumval2a  14475  gsumval3  15207  eltg3  16716  elptr  17284  uptx  17335  alexsubALTlem1  17757  ptcmplem3  17764  prdsxmslem2  18091  itgmcntTMP  23603  relexpindlem  24051  zprodn0  24162  fprod  24164  wfrlem15  24341  fnimage  24539  injrec2  25222  prl  25270  dffprod  25422  indcls2  26099  fnessref  26396  refssfne  26397  filnetlem4  26433  unirep  26452  indexa  26515  fnchoice  27803  stoweidlem5  27857  stoweidlem27  27879  stoweidlem28  27880  stoweidlem31  27883  stoweidlem43  27895  stoweidlem44  27896  stoweidlem51  27903  stoweidlem59  27911
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803
  Copyright terms: Public domain W3C validator