Theorem spcegv 3135

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

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1444   E.wex 1663   e. wcel 1887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047

This theorem is referenced by:  spcev  3141  eqeu  3209  absneu  4046  elpreqprlem  4160  elunii  4203  axpweq  4580  brcogw  5003  breldmg  5040  dmsnopg  5307  fvrnressn  6079  f1oexbi  6743  zfrep6  6761  unielxp  6829  wfrlem15  7050  ertr  7378  f1oen3g  7585  f1dom2g  7587  f1domg  7589  dom3d  7611  fodomr  7723  disjenex  7730  domssex2  7732  domssex  7733  ordiso  8031  fowdom  8086  brwdom2  8088  infeq5i  8141  oncard  8394  cardsn  8403  infxpenc2lem2  8451  dfac8b  8462  dfac8clem  8463  ac10ct  8465  ac5num  8467  acni2  8477  acnlem  8479  finnisoeu  8544  aceq3lem  8551  dfacacn  8571  infpss  8647  cflem  8676  cflecard  8683  cfslb  8696  cofsmo  8699  coftr  8703  alephsing  8706  fin4i  8728  axdc4lem  8885  ac6num  8909  axdclem2  8950  gchi  9049  grothpw  9251  hasheqf1oi  12534  fz1isolem  12624  wrd2f1tovbij  13035  relexpindlem  13126  climeu  13619  fsum  13786  ntrivcvgn0  13954  fprod  13995  isacs1i  15563  mreacs  15564  brcici  15705  initoeu2lem2  15910  gsumval2a  16522  gsumval3lem2  17540  eltg3  19977  elptr  20588  uptx  20640  alexsubALTlem1  21062  ptcmplem3  21069  prdsxmslem2  21544  nbgraf1o0  25174  cusgraexg  25197  cusgrafilem3  25209  sizeusglecusg  25214  wlknwwlknbij2  25442  wlkiswwlkbij2  25449  wwlkextbij  25461  wlknwwlknvbij  25468  clwwlkbij  25527  clwwlkvbij  25529  frgrancvvdeqlem9  25769  numclwlk1lem2  25825  numclwwlk2lem3  25834  rmoeqALT  28123  aciunf1lem  28264  locfinref  28668  fnimage  30696  fnessref  31013  refssfne  31014  filnetlem4  31037  fin2so  31932  unirep  32039  indexa  32060  rp-isfinite5  36162  elabd  36178  choicefi  37481  stoweidlem5  37865  stoweidlem27  37887  stoweidlem28  37888  stoweidlem31  37892  stoweidlem43  37904  stoweidlem44  37905  stoweidlem51  37912  stoweidlem59  37920  issn  38995  nbusgrf1o1  39444  cusgrexg  39508  cusgrfilem3  39518  sizusglecusg  39524  irinitoringc  40124