Theorem spcegv 3294

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

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   E.wex 1704   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202

This theorem is referenced by:  spcev  3300  elabd  3352  eqeu  3377  absneu  4263  issn  4363  elpreqprlem  4395  elunii  4441  axpweq  4842  brcogw  5290  opeldmd  5327  breldmg  5330  dmsnopg  5606  fvrnressn  6428  f1oexbi  7116  zfrep6  7134  unielxp  7204  wfrlem15  7429  ertr  7757  f1oen3g  7971  f1dom2g  7973  f1domg  7975  dom3d  7997  fodomr  8111  disjenex  8118  domssex2  8120  domssex  8121  ordiso  8421  fowdom  8476  brwdom2  8478  infeq5i  8533  oncard  8786  cardsn  8795  infxpenc2lem2  8843  dfac8b  8854  dfac8clem  8855  ac10ct  8857  ac5num  8859  acni2  8869  acnlem  8871  finnisoeu  8936  aceq3lem  8943  dfacacn  8963  infpss  9039  cflem  9068  cflecard  9075  cfslb  9088  cofsmo  9091  coftr  9095  alephsing  9098  fin4i  9120  axdc4lem  9277  ac6num  9301  axdclem2  9342  gchi  9446  grothpw  9648  hasheqf1oi  13140  hasheqf1oiOLD  13141  fz1isolem  13245  wrd2f1tovbij  13703  relexpindlem  13803  climeu  14286  fsum  14451  ntrivcvgn0  14630  fprod  14671  isacs1i  16318  mreacs  16319  brcici  16460  initoeu2lem2  16665  gsumval2a  17279  gsumval3lem2  18307  eltg3  20766  elptr  21376  uptx  21428  alexsubALTlem1  21851  ptcmplem3  21858  prdsxmslem2  22334  nbusgrf1o1  26272  cusgrexg  26340  cusgrfilem3  26353  sizusglecusg  26359  wlknwwlksnbij2  26778  wlkwwlkbij2  26785  wlksnwwlknvbij  26803  clwwlksbij  26920  clwwlksvbij  26922  numclwlk1lem2  27230  rmoeqALT  29327  aciunf1lem  29462  locfinref  29908  fnimage  32036  fnessref  32352  refssfne  32353  filnetlem4  32376  bj-restb  33047  fin2so  33396  unirep  33507  indexa  33528  rp-isfinite5  37863  nssd  39288  choicefi  39392  axccdom  39416  stoweidlem5  40222  stoweidlem27  40244  stoweidlem28  40245  stoweidlem31  40248  stoweidlem43  40260  stoweidlem44  40261  stoweidlem51  40268  stoweidlem59  40276  nsssmfmbflem  40986  sprbisymrel  41749  uspgrbisymrelALT  41763  irinitoringc  42069