Theorem spcegv 2774

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1331   E.wex 1468   e. wcel 1480

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688

This theorem is referenced by:  spcev  2780  elabd  2829  eqeu  2854  absneu  3595  elunii  3741  axpweq  4095  euotd  4176  brcogw  4708  opeldmg  4744  breldmg  4745  dmsnopg  5010  dff3im  5565  elunirn  5667  unielxp  6072  op1steq  6077  tfr0dm  6219  tfrlemibxssdm  6224  tfrlemiex  6228  tfr1onlembxssdm  6240  tfr1onlemex  6244  tfrcllembxssdm  6253  tfrcllemex  6257  frecabcl  6296  ertr  6444  f1oen3g  6648  f1dom2g  6650  f1domg  6652  dom3d  6668  en1  6693  phpelm  6760  isinfinf  6791  ordiso  6921  djudom  6978  difinfsn  6985  ctm  6994  enumct  7000  djudoml  7075  djudomr  7076  recexnq  7198  ltexprlemrl  7418  ltexprlemru  7420  recexprlemm  7432  recexprlemloc  7439  recexprlem1ssl  7441  recexprlem1ssu  7442  axpre-suploclemres  7709  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  fihasheqf1oi  10534  zfz1isolem1  10583  climeu  11065  fsum3  11156  eltg3  12226  uptx  12443  xblm  12586  bj-2inf  13136  subctctexmid  13196