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

Theorem spcegv 2981
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 2524 . 2  |-  F/_ x A
2 nfv 1626 . 2  |-  F/ x ps
3 spcgv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3spcegf 2976 1  |-  ( A  e.  V  ->  ( ps  ->  E. x ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wex 1547    = wceq 1649    e. wcel 1717
This theorem is referenced by:  spcev  2987  eqeu  3049  absneu  3822  elunii  3963  axpweq  4318  brcogw  4982  breldmg  5016  dmsnopg  5282  zfrep6  5908  unielxp  6325  ertr  6857  f1oen3g  7060  f1dom2g  7062  f1domg  7064  dom3d  7086  fodomr  7195  disjenex  7202  domssex2  7204  domssex  7205  ordiso  7419  fowdom  7473  brwdom2  7475  infeq5i  7525  oncard  7781  cardsn  7790  infxpenc2lem2  7835  dfac8b  7846  dfac8clem  7847  ac10ct  7849  ac5num  7851  acni2  7861  acnlem  7863  finnisoeu  7928  aceq3lem  7935  dfacacn  7955  infpss  8031  cflem  8060  cflecard  8067  cfslb  8080  cofsmo  8083  coftr  8087  alephsing  8090  fin4i  8112  axdc4lem  8269  ac6num  8293  axdclem2  8334  gchi  8433  grothpw  8635  hasheqf1oi  11563  fz1isolem  11638  climeu  12277  fsum  12442  isacs1i  13810  mreacs  13811  gsumval2a  14710  gsumval3  15442  eltg3  16951  elptr  17527  uptx  17579  alexsubALTlem1  18000  ptcmplem3  18007  prdsxmslem2  18450  nbgraf1o0  21323  cusgraexg  21345  cusgrafilem3  21357  sizeusglecusg  21362  relexpindlem  24919  ntrivcvgn0  25006  fprod  25047  wfrlem15  25295  fnimage  25493  fnessref  26065  refssfne  26066  filnetlem4  26102  unirep  26106  indexa  26127  stoweidlem5  27423  stoweidlem27  27445  stoweidlem28  27446  stoweidlem31  27449  stoweidlem43  27461  stoweidlem44  27462  stoweidlem51  27469  stoweidlem59  27477  frgrancvvdeqlem9  27794
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902
  Copyright terms: Public domain W3C validator