Theorem spcegv 3199

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   E.wex 1596   e. wcel 1767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115

This theorem is referenced by:  spcev  3205  eqeu  3274  absneu  4101  elunii  4250  axpweq  4624  brcogw  5171  breldmg  5208  dmsnopg  5479  fvrnressn  6076  f1oexbi  6734  zfrep6  6752  unielxp  6820  ertr  7326  f1oen3g  7531  f1dom2g  7533  f1domg  7535  dom3d  7557  fodomr  7668  disjenex  7675  domssex2  7677  domssex  7678  ordiso  7941  fowdom  7997  brwdom2  7999  infeq5i  8053  oncard  8341  cardsn  8350  infxpenc2lem2  8397  infxpenc2lem2OLD  8401  dfac8b  8412  dfac8clem  8413  ac10ct  8415  ac5num  8417  acni2  8427  acnlem  8429  finnisoeu  8494  aceq3lem  8501  dfacacn  8521  infpss  8597  cflem  8626  cflecard  8633  cfslb  8646  cofsmo  8649  coftr  8653  alephsing  8656  fin4i  8678  axdc4lem  8835  ac6num  8859  axdclem2  8900  gchi  9002  grothpw  9204  hasheqf1oi  12392  fz1isolem  12476  wrd2f1tovbij  12861  climeu  13341  fsum  13505  isacs1i  14912  mreacs  14913  gsumval2a  15834  gsumval3OLD  16711  gsumval3lem2  16713  eltg3  19258  elptr  19837  uptx  19889  alexsubALTlem1  20310  ptcmplem3  20317  prdsxmslem2  20795  nbgraf1o0  24150  cusgraexg  24173  cusgrafilem3  24185  sizeusglecusg  24190  wlknwwlknbij2  24418  wlkiswwlkbij2  24425  wwlkextbij  24437  wlknwwlknvbij  24444  clwwlkbij  24503  clwwlkvbij  24505  frgrancvvdeqlem9  24746  numclwlk1lem2  24802  numclwwlk2lem3  24811  rmoeq  27090  cnvoprab  27246  relexpindlem  28565  ntrivcvgn0  28637  fprod  28678  wfrlem15  28962  fnimage  29184  fin2so  29645  fnessref  29793  refssfne  29794  filnetlem4  29830  unirep  29834  indexa  29855  stoweidlem5  31333  stoweidlem27  31355  stoweidlem28  31356  stoweidlem31  31359  stoweidlem43  31371  stoweidlem44  31372  stoweidlem51  31379  stoweidlem59  31387