Theorem spcev 3300

Description: Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypotheses

Ref	Expression
spcv.1	|- A e. _V
spcv.2	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
spcev	|- ( ps -> E. x ph )

Distinct variable groups:   x, A   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem spcev

Step	Hyp	Ref	Expression
1		spcv.1	. 2 |- A e. _V
2		spcv.2	. . 3 |- ( x = A -> ( ph <-> ps ) )
3	2	spcegv 3294	. 2 |- ( A e. _V -> ( ps -> E. x ph ) )
4	1, 3	ax-mp 5	1 |- ( ps -> E. x ph )

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

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:  dtruALT  4899  elALT  4910  dtruALT2  4911  nnullss  4930  exss  4931  euotd  4975  opeldm  5328  elrnmpt1  5374  xpnz  5553  ssimaex  6263  fvelrn  6352  dff3  6372  exfo  6377  eufnfv  6491  elunirn  6509  fsnex  6538  f1prex  6539  foeqcnvco  6555  snnexOLD  6967  ffoss  7127  op1steq  7210  frxp  7287  suppimacnv  7306  seqomlem2  7546  domtr  8009  ensn1  8020  en1  8023  enfixsn  8069  php3  8146  1sdom  8163  isinf  8173  ssfi  8180  ac6sfi  8204  hartogslem1  8447  brwdom2  8478  inf0  8518  axinf2  8537  cnfcom3clem  8602  tz9.1  8605  tz9.1c  8606  rankuni  8726  scott0  8749  cplem2  8753  bnd2  8756  karden  8758  cardprclem  8805  dfac4  8945  dfac5lem5  8950  dfac5  8951  dfac2a  8952  dfac2  8953  kmlem2  8973  kmlem13  8984  ackbij2  9065  cfsuc  9079  cfflb  9081  cfss  9087  cfsmolem  9092  cfcoflem  9094  fin23lem32  9166  axcc2lem  9258  axcc3  9260  axdc2lem  9270  axdc3lem2  9273  axcclem  9279  brdom3  9350  brdom7disj  9353  brdom6disj  9354  axpowndlem3  9421  canthnumlem  9470  canthp1lem2  9475  inar1  9597  recmulnq  9786  ltexnq  9797  halfnq  9798  ltbtwnnq  9800  1idpr  9851  ltexprlem7  9864  reclem2pr  9870  reclem3pr  9871  sup2  10979  nnunb  11288  uzrdgfni  12757  axdc4uzlem  12782  rtrclreclem3  13800  ntrivcvgmullem  14633  fprodntriv  14672  cnso  14976  vdwapun  15678  vdwlem1  15685  vdwlem12  15696  vdwlem13  15697  isacs2  16314  equivestrcsetc  16792  psgneu  17926  efglem  18129  lmisfree  20181  toprntopon  20729  neitr  20984  cmpsublem  21202  cmpsub  21203  bwth  21213  1stcfb  21248  unisngl  21330  alexsubALTlem3  21853  alexsubALTlem4  21854  vitali  23382  mbfi1fseqlem6  23487  mbfi1flimlem  23489  aannenlem2  24084  istrkg2ld  25359  axlowdim  25841  wlkpwwlkf1ouspgr  26765  wlkisowwlkupgr  26766  padct  29497  cnvoprab  29498  f1ocnt  29559  locfinreflem  29907  locfinref  29908  prsdm  29960  prsrn  29961  eulerpart  30444  bnj150  30946  trpredpred  31728  nosupno  31849  nosupfv  31852  fnsingle  32026  finminlem  32312  filnetlem3  32375  cnndvlem2  32529  bj-restpw  33045  bj-rest0  33046  poimirlem2  33411  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2addnclem  33461  itg2addnc  33464  indexdom  33529  sdclem2  33538  fdc  33541  prtlem16  34154  dihglblem2aN  36582  eldioph2lem2  37324  dford3lem2  37594  aomclem7  37630  dfac11  37632  relintabex  37887  rclexi  37922  trclexi  37927  rtrclexi  37928  fnchoice  39188  ssnnf1octb  39382  fzisoeu  39514  stoweidlem28  40245  nnfoctbdjlem  40672  smfpimcclem  41013  setrec1lem3  42436  setrec2lem2  42441