Theorem spcegv 2777

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

Step	Hyp	Ref	Expression
1		nfcv 2282	. 2 |- F/_ x A
2		nfv 1509	. 2 |- F/ x ps
3		spcgv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
4	1, 2, 3	spcegf 2772	1 |- ( A e. V -> ( ps -> E. x ph ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1332   E.wex 1469   e. wcel 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691

This theorem is referenced by:  spcedv  2778  spcev  2784  elabd  2833  eqeu  2858  absneu  3603  elunii  3749  axpweq  4103  euotd  4184  brcogw  4716  opeldmg  4752  breldmg  4753  dmsnopg  5018  dff3im  5573  elunirn  5675  unielxp  6080  op1steq  6085  tfr0dm  6227  tfrlemibxssdm  6232  tfrlemiex  6236  tfr1onlembxssdm  6248  tfr1onlemex  6252  tfrcllembxssdm  6261  tfrcllemex  6265  frecabcl  6304  ertr  6452  f1oen3g  6656  f1dom2g  6658  f1domg  6660  dom3d  6676  en1  6701  phpelm  6768  isinfinf  6799  ordiso  6929  djudom  6986  difinfsn  6993  ctm  7002  enumct  7008  djudoml  7092  djudomr  7093  cc2lem  7098  recexnq  7222  ltexprlemrl  7442  ltexprlemru  7444  recexprlemm  7456  recexprlemloc  7463  recexprlem1ssl  7465  recexprlem1ssu  7466  axpre-suploclemres  7733  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  fihasheqf1oi  10566  zfz1isolem1  10615  climeu  11097  fsum3  11188  eltg3  12265  uptx  12482  xblm  12625  bj-2inf  13307  subctctexmid  13369