Theorem spcegv 2800

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1335   E.wex 1472   e. wcel 2128

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714

This theorem is referenced by:  spcedv  2801  spcev  2807  elabd  2857  eqeu  2882  absneu  3633  elunii  3779  axpweq  4134  euotd  4216  brcogw  4757  opeldmg  4793  breldmg  4794  dmsnopg  5059  dff3im  5614  elunirn  5718  unielxp  6124  op1steq  6129  tfr0dm  6271  tfrlemibxssdm  6276  tfrlemiex  6280  tfr1onlembxssdm  6292  tfr1onlemex  6296  tfrcllembxssdm  6305  tfrcllemex  6309  frecabcl  6348  ertr  6497  f1oen3g  6701  f1dom2g  6703  f1domg  6705  dom3d  6721  en1  6746  phpelm  6813  isinfinf  6844  ordiso  6982  djudom  7039  difinfsn  7046  ctm  7055  enumct  7061  djudoml  7156  djudomr  7157  cc2lem  7188  recexnq  7312  ltexprlemrl  7532  ltexprlemru  7534  recexprlemm  7546  recexprlemloc  7553  recexprlem1ssl  7555  recexprlem1ssu  7556  axpre-suploclemres  7823  frecuzrdgtcl  10320  frecuzrdgfunlem  10327  fihasheqf1oi  10673  zfz1isolem1  10722  climeu  11204  fsum3  11295  eltg3  12527  uptx  12744  xblm  12887  bj-2inf  13584  subctctexmid  13644