Theorem spcegv 3047

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1362   E.wex 1589   e. wcel 1755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964

This theorem is referenced by:  spcev  3053  eqeu  3119  absneu  3937  elunii  4084  axpweq  4457  brcogw  4995  breldmg  5032  dmsnopg  5298  zfrep6  6534  unielxp  6601  ertr  7104  f1oen3g  7313  f1dom2g  7315  f1domg  7317  dom3d  7339  fodomr  7450  disjenex  7457  domssex2  7459  domssex  7460  ordiso  7718  fowdom  7774  brwdom2  7776  infeq5i  7830  oncard  8118  cardsn  8127  infxpenc2lem2  8174  infxpenc2lem2OLD  8178  dfac8b  8189  dfac8clem  8190  ac10ct  8192  ac5num  8194  acni2  8204  acnlem  8206  finnisoeu  8271  aceq3lem  8278  dfacacn  8298  infpss  8374  cflem  8403  cflecard  8410  cfslb  8423  cofsmo  8426  coftr  8430  alephsing  8433  fin4i  8455  axdc4lem  8612  ac6num  8636  axdclem2  8677  gchi  8778  grothpw  8980  hasheqf1oi  12105  fz1isolem  12197  climeu  13016  fsum  13180  isacs1i  14577  mreacs  14578  gsumval2a  15491  gsumval3OLD  16361  gsumval3lem2  16363  eltg3  18408  elptr  18987  uptx  19039  alexsubALTlem1  19460  ptcmplem3  19467  prdsxmslem2  19945  nbgraf1o0  23177  cusgraexg  23199  cusgrafilem3  23211  sizeusglecusg  23216  rmoeq  25694  cnvoprab  25846  relexpindlem  27187  ntrivcvgn0  27259  fprod  27300  wfrlem15  27584  fnimage  27806  fin2so  28257  fnessref  28406  refssfne  28407  filnetlem4  28443  unirep  28447  indexa  28468  stoweidlem5  29643  stoweidlem27  29665  stoweidlem28  29666  stoweidlem31  29669  stoweidlem43  29681  stoweidlem44  29682  stoweidlem51  29689  stoweidlem59  29697  fvelrnfvelrnressn  29994  f1oexbi  29999  wrd2f1tovbij  30098  wlknwwlknbij2  30189  wlkiswwlkbij2  30196  wwlkextbij  30208  wlknwwlknvbij  30215  clwwlkbij  30304  clwwlkvbij  30306  frgrancvvdeqlem9  30477  numclwlk1lem2  30533  numclwwlk2lem3  30542