Theorem spcev 3597

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	⊢ 𝐴 ∈ V
spcv.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spcev	⊢ (𝜓 → ∃𝑥𝜑)

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem spcev

Step	Hyp	Ref	Expression
1		spcv.1	. 2 ⊢ 𝐴 ∈ V
2		spcv.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	spcegv 3588	. 2 ⊢ (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
4	1, 3	ax-mp 5	1 ⊢ (𝜓 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wex 1779   ∈ wcel 2104  Vcvv 3472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-clel 2808

This theorem is referenced by:  dtruALT  5387  nnullss  5463  exss  5464  euotd  5514  opeldm  5908  elrnmpt1  5958  xpnz  6159  ssimaex  6977  fvelrn  7079  dff3  7102  exfo  7107  eufnfv  7234  elunirn  7254  fsnex  7285  f1prex  7286  foeqcnvco  7302  ffoss  7936  op1steq  8023  frxp  8116  suppimacnv  8163  seqomlem2  8455  domtr  9007  en1  9025  en1OLD  9026  enfixsn  9085  ssfiALT  9178  php3  9216  php3OLD  9228  1sdomOLD  9253  isinf  9264  isinfOLD  9265  ac6sfi  9291  hartogslem1  9541  brwdom2  9572  inf0  9620  axinf2  9639  cnfcom3clem  9704  ssttrcl  9714  ttrcltr  9715  ttrclss  9719  ttrclselem2  9725  tz9.1c  9729  rankuni  9862  scott0  9885  bnd2  9892  cardprclem  9978  dfac4  10121  dfac5lem5  10126  dfac5  10127  dfac2a  10128  dfac2b  10129  kmlem2  10150  kmlem13  10161  ackbij2  10242  cfsuc  10256  cfflb  10258  cfss  10264  cfsmolem  10269  cfcoflem  10271  fin23lem32  10343  axcc2lem  10435  axcc3  10437  axdc2lem  10447  axdc3lem2  10450  axcclem  10456  brdom3  10527  brdom7disj  10530  brdom6disj  10531  axpowndlem3  10598  canthnumlem  10647  canthp1lem2  10652  inar1  10774  recmulnq  10963  ltexnq  10974  halfnq  10975  ltbtwnnq  10977  1idpr  11028  ltexprlem7  11041  reclem2pr  11047  reclem3pr  11048  sup2  12176  nnunb  12474  uzrdgfni  13929  axdc4uzlem  13954  rtrclreclem3  15013  ntrivcvgmullem  15853  fprodntriv  15892  cnso  16196  vdwapun  16913  vdwlem1  16920  vdwlem12  16931  vdwlem13  16932  isacs2  17603  equivestrcsetc  18110  psgneu  19417  efglem  19627  lmisfree  21618  toprntopon  22649  neitr  22906  cmpsublem  23125  cmpsub  23126  bwth  23136  1stcfb  23171  unisngl  23253  alexsubALTlem3  23775  alexsubALTlem4  23776  vitali  25364  mbfi1fseqlem6  25472  mbfi1flimlem  25474  aannenlem2  26076  nosupno  27440  nosupfv  27443  noinfno  27455  noinffv  27458  istrkg2ld  27976  axlowdim  28484  wlkswwlksf1o  29398  clwlkclwwlkf  29526  padct  32209  cnvoprabOLD  32210  f1ocnt  32278  cycpmconjslem2  32582  locfinreflem  33116  locfinref  33117  prsdm  33190  prsrn  33191  eulerpart  33677  fineqvac  34393  satf0op  34664  prv1n  34718  fnsingle  35193  finminlem  35508  filnetlem3  35570  cnndvlem2  35719  bj-restpw  36278  bj-rest0  36279  exrecfnlem  36565  ctbssinf  36592  poimirlem2  36795  mblfinlem3  36832  mblfinlem4  36833  ismblfin  36834  itg2addnclem  36844  itg2addnc  36847  indexdom  36907  sdclem2  36915  fdc  36918  prtlem16  38044  dihglblem2aN  40469  sn-sup2  41646  eldioph2lem2  41803  dford3lem2  42070  aomclem7  42106  dfac11  42108  rclexi  42670  trclexi  42675  rtrclexi  42676  fnchoice  44017  ssnnf1octb  44193  fzisoeu  44310  stoweidlem28  45044  nnfoctbdjlem  45471  smfpimcclem  45823  funressndmafv2rn  46231  mof0  47593  setc2othin  47765  setrec1lem3  47823  setrec2lem2  47828