Theorem spcegv 3079

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1369   E.wex 1586   e. wcel 1756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995

This theorem is referenced by:  spcev  3085  eqeu  3151  absneu  3970  elunii  4117  axpweq  4490  brcogw  5029  breldmg  5066  dmsnopg  5331  zfrep6  6566  unielxp  6633  ertr  7137  f1oen3g  7346  f1dom2g  7348  f1domg  7350  dom3d  7372  fodomr  7483  disjenex  7490  domssex2  7492  domssex  7493  ordiso  7751  fowdom  7807  brwdom2  7809  infeq5i  7863  oncard  8151  cardsn  8160  infxpenc2lem2  8207  infxpenc2lem2OLD  8211  dfac8b  8222  dfac8clem  8223  ac10ct  8225  ac5num  8227  acni2  8237  acnlem  8239  finnisoeu  8304  aceq3lem  8311  dfacacn  8331  infpss  8407  cflem  8436  cflecard  8443  cfslb  8456  cofsmo  8459  coftr  8463  alephsing  8466  fin4i  8488  axdc4lem  8645  ac6num  8669  axdclem2  8710  gchi  8812  grothpw  9014  hasheqf1oi  12143  fz1isolem  12235  climeu  13054  fsum  13218  isacs1i  14616  mreacs  14617  gsumval2a  15533  gsumval3OLD  16403  gsumval3lem2  16405  eltg3  18589  elptr  19168  uptx  19220  alexsubALTlem1  19641  ptcmplem3  19648  prdsxmslem2  20126  nbgraf1o0  23377  cusgraexg  23399  cusgrafilem3  23411  sizeusglecusg  23416  rmoeq  25893  cnvoprab  26045  relexpindlem  27363  ntrivcvgn0  27435  fprod  27476  wfrlem15  27760  fnimage  27982  fin2so  28442  fnessref  28591  refssfne  28592  filnetlem4  28628  unirep  28632  indexa  28653  stoweidlem5  29826  stoweidlem27  29848  stoweidlem28  29849  stoweidlem31  29852  stoweidlem43  29864  stoweidlem44  29865  stoweidlem51  29872  stoweidlem59  29880  fvelrnfvelrnressn  30177  f1oexbi  30182  wrd2f1tovbij  30281  wlknwwlknbij2  30372  wlkiswwlkbij2  30379  wwlkextbij  30391  wlknwwlknvbij  30398  clwwlkbij  30487  clwwlkvbij  30489  frgrancvvdeqlem9  30660  numclwlk1lem2  30716  numclwwlk2lem3  30725