Theorem spcev 3548

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 3539	. 2 ⊢ (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
4	1, 3	ax-mp 5	1 ⊢ (𝜓 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-clel 2811

This theorem is referenced by:  dtruALT  5330  nnullss  5414  exss  5415  euotd  5467  opeldm  5862  elrnmpt1  5915  xpnz  6123  ssimaex  6925  fvelrn  7028  dff3  7052  exfo  7057  eufnfv  7184  elunirn  7206  fsnex  7238  f1prex  7239  foeqcnvco  7255  ffoss  7899  op1steq  7986  frxp  8076  suppimacnv  8124  seqomlem2  8390  domtr  8954  en1  8971  enfixsn  9024  ssfiALT  9108  php3  9143  isinf  9175  ac6sfi  9194  hartogslem1  9457  brwdom2  9488  inf0  9542  axinf2  9561  cnfcom3clem  9626  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  tz9.1c  9651  rankuni  9787  scott0  9810  bnd2  9817  cardprclem  9903  dfac4  10044  dfac5lem5  10049  dfac5  10051  dfac2a  10052  dfac2b  10053  kmlem2  10074  kmlem13  10085  ackbij2  10164  cfsuc  10179  cfflb  10181  cfss  10187  cfsmolem  10192  cfcoflem  10194  fin23lem32  10266  axcc2lem  10358  axcc3  10360  axdc2lem  10370  axdc3lem2  10373  axcclem  10379  brdom3  10450  brdom7disj  10453  brdom6disj  10454  axpowndlem3  10522  canthnumlem  10571  canthp1lem2  10576  inar1  10698  recmulnq  10887  ltexnq  10898  halfnq  10899  ltbtwnnq  10901  1idpr  10952  ltexprlem7  10965  reclem2pr  10971  reclem3pr  10972  sup2  12112  nnunb  12433  uzrdgfni  13920  axdc4uzlem  13945  rtrclreclem3  15022  ntrivcvgmullem  15866  fprodntriv  15907  cnso  16214  vdwapun  16945  vdwlem1  16952  vdwlem12  16963  vdwlem13  16964  isacs2  17619  equivestrcsetc  18118  psgneu  19481  efglem  19691  lmisfree  21822  toprntopon  22890  neitr  23145  cmpsublem  23364  cmpsub  23365  bwth  23375  1stcfb  23410  unisngl  23492  alexsubALTlem3  24014  alexsubALTlem4  24015  vitali  25580  mbfi1fseqlem6  25687  mbfi1flimlem  25689  aannenlem2  26295  nosupno  27667  nosupfv  27670  noinfno  27682  noinffv  27685  noseqrdgfn  28298  istrkg2ld  28528  axlowdim  29030  wlkswwlksf1o  29947  clwlkclwwlkf  30078  padct  32791  f1ocnt  32873  cycpmconjslem2  33216  locfinreflem  33984  locfinref  33985  prsdm  34058  prsrn  34059  eulerpart  34526  fineqvac  35260  satf0op  35559  prv1n  35613  fnsingle  36099  finminlem  36500  filnetlem3  36562  dfttc4lem1  36710  regsfromregtco  36720  cnndvlem2  36798  bj-restpw  37404  bj-rest0  37405  exrecfnlem  37695  ctbssinf  37722  poimirlem2  37943  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  itg2addnclem  37992  itg2addnc  37995  indexdom  38055  sdclem2  38063  fdc  38066  prtlem16  39315  dihglblem2aN  41739  sn-sup2  42936  eldioph2lem2  43193  dford3lem2  43455  aomclem7  43488  dfac11  43490  rclexi  44042  trclexi  44047  rtrclexi  44048  permaxinf2lem  45439  permac8prim  45441  fnchoice  45460  ssnnf1octb  45624  fzisoeu  45733  stoweidlem28  46456  nnfoctbdjlem  46883  smfpimcclem  47235  funressndmafv2rn  47671  mof0  49313  nelsubc3lem  49545  initc  49566  setc2othin  49941  cnelsubclem  50078  setrec1lem3  50164  setrec2lem2  50169