Theorem spcev 3585

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3459

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 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-clel 2809

This theorem is referenced by:  dtruALT  5358  nnullss  5437  exss  5438  euotd  5488  opeldm  5887  elrnmpt1  5940  xpnz  6148  ssimaex  6963  fvelrn  7065  dff3  7089  exfo  7094  eufnfv  7220  elunirn  7242  fsnex  7275  f1prex  7276  foeqcnvco  7292  ffoss  7942  op1steq  8030  frxp  8123  suppimacnv  8171  seqomlem2  8463  domtr  9019  en1  9036  enfixsn  9093  ssfiALT  9186  php3  9221  php3OLD  9231  1sdomOLD  9255  isinf  9266  isinfOLD  9267  ac6sfi  9290  hartogslem1  9554  brwdom2  9585  inf0  9633  axinf2  9652  cnfcom3clem  9717  ssttrcl  9727  ttrcltr  9728  ttrclss  9732  ttrclselem2  9738  tz9.1c  9742  rankuni  9875  scott0  9898  bnd2  9905  cardprclem  9991  dfac4  10134  dfac5lem5  10139  dfac5  10141  dfac2a  10142  dfac2b  10143  kmlem2  10164  kmlem13  10175  ackbij2  10254  cfsuc  10269  cfflb  10271  cfss  10277  cfsmolem  10282  cfcoflem  10284  fin23lem32  10356  axcc2lem  10448  axcc3  10450  axdc2lem  10460  axdc3lem2  10463  axcclem  10469  brdom3  10540  brdom7disj  10543  brdom6disj  10544  axpowndlem3  10611  canthnumlem  10660  canthp1lem2  10665  inar1  10787  recmulnq  10976  ltexnq  10987  halfnq  10988  ltbtwnnq  10990  1idpr  11041  ltexprlem7  11054  reclem2pr  11060  reclem3pr  11061  sup2  12196  nnunb  12495  uzrdgfni  13974  axdc4uzlem  13999  rtrclreclem3  15077  ntrivcvgmullem  15915  fprodntriv  15956  cnso  16263  vdwapun  16992  vdwlem1  16999  vdwlem12  17010  vdwlem13  17011  isacs2  17663  equivestrcsetc  18162  psgneu  19485  efglem  19695  lmisfree  21800  toprntopon  22861  neitr  23116  cmpsublem  23335  cmpsub  23336  bwth  23346  1stcfb  23381  unisngl  23463  alexsubALTlem3  23985  alexsubALTlem4  23986  vitali  25564  mbfi1fseqlem6  25671  mbfi1flimlem  25673  aannenlem2  26287  nosupno  27665  nosupfv  27668  noinfno  27680  noinffv  27683  noseqrdgfn  28229  istrkg2ld  28385  axlowdim  28886  wlkswwlksf1o  29807  clwlkclwwlkf  29935  padct  32643  f1ocnt  32725  cycpmconjslem2  33112  locfinreflem  33817  locfinref  33818  prsdm  33891  prsrn  33892  eulerpart  34360  fineqvac  35074  satf0op  35345  prv1n  35399  fnsingle  35883  finminlem  36282  filnetlem3  36344  cnndvlem2  36502  bj-restpw  37056  bj-rest0  37057  exrecfnlem  37343  ctbssinf  37370  poimirlem2  37592  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  itg2addnclem  37641  itg2addnc  37644  indexdom  37704  sdclem2  37712  fdc  37715  prtlem16  38833  dihglblem2aN  41258  sn-sup2  42461  eldioph2lem2  42731  dford3lem2  42998  aomclem7  43031  dfac11  43033  rclexi  43586  trclexi  43591  rtrclexi  43592  permaxinf2lem  44985  fnchoice  45001  ssnnf1octb  45166  fzisoeu  45277  stoweidlem28  46005  nnfoctbdjlem  46432  smfpimcclem  46784  funressndmafv2rn  47200  mof0  48764  nelsubc3lem  48985  setc2othin  49300  cnelsubclem  49428  setrec1lem3  49501  setrec2lem2  49506