Theorem spcev 3554

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  ∃wex 1780   ∈ wcel 2105  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-clel 2814

This theorem is referenced by:  dtruALT  5332  nnullss  5408  exss  5409  euotd  5458  opeldm  5850  elrnmpt1  5900  xpnz  6098  ssimaex  6910  fvelrn  7011  dff3  7033  exfo  7038  eufnfv  7162  elunirn  7181  fsnex  7212  f1prex  7213  foeqcnvco  7229  ffoss  7857  op1steq  7944  frxp  8035  suppimacnv  8061  seqomlem2  8353  domtr  8869  en1  8887  en1OLD  8888  enfixsn  8947  ssfiALT  9040  php3  9078  php3OLD  9090  1sdomOLD  9115  isinf  9126  isinfOLD  9127  ac6sfi  9153  hartogslem1  9400  brwdom2  9431  inf0  9479  axinf2  9498  cnfcom3clem  9563  ssttrcl  9573  ttrcltr  9574  ttrclss  9578  ttrclselem2  9584  tz9.1c  9588  rankuni  9721  scott0  9744  bnd2  9751  cardprclem  9837  dfac4  9980  dfac5lem5  9985  dfac5  9986  dfac2a  9987  dfac2b  9988  kmlem2  10009  kmlem13  10020  ackbij2  10101  cfsuc  10115  cfflb  10117  cfss  10123  cfsmolem  10128  cfcoflem  10130  fin23lem32  10202  axcc2lem  10294  axcc3  10296  axdc2lem  10306  axdc3lem2  10309  axcclem  10315  brdom3  10386  brdom7disj  10389  brdom6disj  10390  axpowndlem3  10457  canthnumlem  10506  canthp1lem2  10511  inar1  10633  recmulnq  10822  ltexnq  10833  halfnq  10834  ltbtwnnq  10836  1idpr  10887  ltexprlem7  10900  reclem2pr  10906  reclem3pr  10907  sup2  12033  nnunb  12331  uzrdgfni  13780  axdc4uzlem  13805  rtrclreclem3  14871  ntrivcvgmullem  15713  fprodntriv  15752  cnso  16056  vdwapun  16773  vdwlem1  16780  vdwlem12  16791  vdwlem13  16792  isacs2  17460  equivestrcsetc  17967  psgneu  19211  efglem  19418  lmisfree  21156  toprntopon  22181  neitr  22438  cmpsublem  22657  cmpsub  22658  bwth  22668  1stcfb  22703  unisngl  22785  alexsubALTlem3  23307  alexsubALTlem4  23308  vitali  24884  mbfi1fseqlem6  24992  mbfi1flimlem  24994  aannenlem2  25596  nosupno  26958  nosupfv  26961  noinfno  26973  noinffv  26976  istrkg2ld  27111  axlowdim  27619  wlkswwlksf1o  28533  clwlkclwwlkf  28661  padct  31341  cnvoprabOLD  31342  f1ocnt  31410  cycpmconjslem2  31709  locfinreflem  32088  locfinref  32089  prsdm  32162  prsrn  32163  eulerpart  32649  fineqvac  33365  satf0op  33638  prv1n  33692  fnsingle  34360  finminlem  34646  filnetlem3  34708  cnndvlem2  34857  bj-restpw  35419  bj-rest0  35420  exrecfnlem  35706  ctbssinf  35733  poimirlem2  35935  mblfinlem3  35972  mblfinlem4  35973  ismblfin  35974  itg2addnclem  35984  itg2addnc  35987  indexdom  36048  sdclem2  36056  fdc  36059  prtlem16  37187  dihglblem2aN  39612  sn-sup2  40750  eldioph2lem2  40896  dford3lem2  41163  aomclem7  41199  dfac11  41201  rclexi  41596  trclexi  41601  rtrclexi  41602  fnchoice  42945  ssnnf1octb  43112  fzisoeu  43226  stoweidlem28  43957  nnfoctbdjlem  44382  smfpimcclem  44734  funressndmafv2rn  45133  mof0  46583  setc2othin  46755  setrec1lem3  46813  setrec2lem2  46818