Theorem spcev 3574

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ∃wex 1806   ∈ wcel 2149  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-clel 2844

This theorem is referenced by:  dtruALT  5360  nnullss  5444  exss  5445  euotd  5497  opeldm  5898  elrnmpt1  5951  xpnz  6157  ssimaex  6967  fvelrn  7072  dff3  7096  exfo  7101  eufnfv  7228  elunirn  7250  fsnex  7282  f1prex  7283  foeqcnvco  7299  ffoss  7942  op1steq  8029  frxp  8121  suppimacnv  8169  seqomlem2  8437  domtr  9003  en1  9020  enfixsn  9073  ssfiALT  9157  php3  9192  isinf  9224  ac6sfi  9243  hartogslem1  9503  brwdom2  9534  inf0  9589  axinf2  9608  cnfcom3clem  9673  ssttrcl  9683  ttrcltr  9684  ttrclss  9688  ttrclselem2  9694  tz9.1c  9698  rankuni  9834  scott0  9859  bnd2  9878  cardprclem  9964  dfac4  10105  dfac5lem5  10110  dfac5  10111  dfac2a  10112  dfac2b  10113  kmlem2  10134  kmlem13  10145  ackbij2  10224  cfsuc  10240  cfflb  10242  cfss  10248  cfsmolem  10253  cfcoflem  10255  fin23lem32  10327  axcc2lem  10419  axcc3  10421  axdc2lem  10431  axdc3lem2  10434  axcclem  10440  brdom3  10511  brdom7disj  10514  brdom6disj  10515  axpowndlem3  10583  canthnumlem  10632  canthp1lem2  10637  inar1  10759  recmulnq  10948  ltexnq  10959  halfnq  10960  ltbtwnnq  10962  1idpr  11013  ltexprlem7  11026  reclem2pr  11032  reclem3pr  11033  sup2  12170  nnunb  12499  uzrdgfni  13993  axdc4uzlem  14018  rtrclreclem3  15096  ntrivcvgmullem  15954  fprodntriv  15995  cnso  16302  vdwapun  17033  vdwlem1  17040  vdwlem12  17051  vdwlem13  17052  isacs2  17708  equivestrcsetc  18207  psgneu  19575  efglem  19785  lmisfree  21960  toprntopon  23050  neitr  23305  cmpsublem  23524  cmpsub  23525  bwth  23535  1stcfb  23570  unisngl  23652  alexsubALTlem3  24174  alexsubALTlem4  24175  vitali  25740  mbfi1fseqlem6  25847  mbfi1flimlem  25849  aannenlem2  26458  nosupno  27832  nosupfv  27835  noinfno  27847  noinffv  27850  noseqrdgfn  28464  istrkg2ld  28694  axlowdim  29251  wlkswwlksf1o  30168  clwlkclwwlkf  30299  padct  33003  f1ocnt  33085  cycpmconjslem2  33415  locfinreflem  34174  locfinref  34175  prsdm  34248  prsrn  34249  eulerpart  34716  fineqvac  35451  satf0op  35767  prv1n  35821  fnsingle  36307  finminlem  36717  filnetlem3  36779  dfttc4lem1  36927  regsfromregtco  36937  cnndvlem2  37015  bj-restpw  37621  bj-rest0  37622  exrecfnlem  37912  ctbssinf  37939  poimirlem2  38160  mblfinlem3  38197  mblfinlem4  38198  ismblfin  38199  itg2addnclem  38209  itg2addnc  38212  indexdom  38272  sdclem2  38280  fdc  38283  prtlem16  39532  dihglblem2aN  41956  sn-sup2  43154  eldioph2lem2  43383  dford3lem2  43645  aomclem7  43678  dfac11  43680  rclexi  44232  trclexi  44237  rtrclexi  44238  permaxinf2lem  45612  permac8prim  45614  fnchoice  45640  ssnnf1octb  45803  fzisoeu  45910  stoweidlem28  46633  nnfoctbdjlem  47060  smfpimcclem  47412  funressndmafv2rn  47848  mof0  49500  nelsubc3lem  49732  initc  49753  setc2othin  50128  cnelsubclem  50265  setrec1lem3  50351  setrec2lem2  50356