Theorem spcegv 3179

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1381   E.wex 1597   e. wcel 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095

This theorem is referenced by:  spcev  3185  eqeu  3254  absneu  4085  elunii  4235  axpweq  4610  brcogw  5157  breldmg  5194  dmsnopg  5465  fvrnressn  6067  f1oexbi  6731  zfrep6  6749  unielxp  6817  ertr  7324  f1oen3g  7529  f1dom2g  7531  f1domg  7533  dom3d  7555  fodomr  7666  disjenex  7673  domssex2  7675  domssex  7676  ordiso  7939  fowdom  7995  brwdom2  7997  infeq5i  8051  oncard  8339  cardsn  8348  infxpenc2lem2  8395  infxpenc2lem2OLD  8399  dfac8b  8410  dfac8clem  8411  ac10ct  8413  ac5num  8415  acni2  8425  acnlem  8427  finnisoeu  8492  aceq3lem  8499  dfacacn  8519  infpss  8595  cflem  8624  cflecard  8631  cfslb  8644  cofsmo  8647  coftr  8651  alephsing  8654  fin4i  8676  axdc4lem  8833  ac6num  8857  axdclem2  8898  gchi  9000  grothpw  9202  hasheqf1oi  12398  fz1isolem  12484  wrd2f1tovbij  12872  climeu  13352  fsum  13516  isacs1i  14926  mreacs  14927  gsumval2a  15775  gsumval3OLD  16777  gsumval3lem2  16779  eltg3  19330  elptr  19940  uptx  19992  alexsubALTlem1  20413  ptcmplem3  20420  prdsxmslem2  20898  nbgraf1o0  24311  cusgraexg  24334  cusgrafilem3  24346  sizeusglecusg  24351  wlknwwlknbij2  24579  wlkiswwlkbij2  24586  wwlkextbij  24598  wlknwwlknvbij  24605  clwwlkbij  24664  clwwlkvbij  24666  frgrancvvdeqlem9  24906  numclwlk1lem2  24962  numclwwlk2lem3  24971  rmoeq  27251  locfinref  27710  relexpindlem  28928  ntrivcvgn0  29000  fprod  29041  wfrlem15  29325  fnimage  29547  fin2so  30008  fnessref  30143  refssfne  30144  filnetlem4  30167  unirep  30171  indexa  30192  stoweidlem5  31672  stoweidlem27  31694  stoweidlem28  31695  stoweidlem31  31698  stoweidlem43  31710  stoweidlem44  31711  stoweidlem51  31718  stoweidlem59  31726  rp-isfinite5  37408