Theorem spcegv 2686

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 2219	. 2 |- F/_ x A
2		nfv 1461	. 2 |- F/ x ps
3		spcgv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
4	1, 2, 3	spcegf 2681	1 |- ( A e. V -> ( ps -> E. x ph ) )

Syntax hints:   -> wi 4   <-> wb 103   = wceq 1284   E.wex 1421   e. wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603

This theorem is referenced by:  spcev  2692  eqeu  2762  absneu  3464  elunii  3606  axpweq  3945  euotd  4009  brcogw  4522  opeldmg  4558  breldmg  4559  dmsnopg  4812  dff3im  5333  elunirn  5426  unielxp  5820  op1steq  5825  tfr0  5960  tfrlemibxssdm  5964  tfrlemiex  5968  ertr  6144  f1oen3g  6257  f1dom2g  6259  f1domg  6261  dom3d  6277  en1  6302  phpelm  6352  ordiso  6447  recexnq  6580  ltexprlemrl  6800  ltexprlemru  6802  recexprlemm  6814  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  frecuzrdgfn  9414  climeu  10135  bj-2inf  10733