Theorem spcedv 3611

Description: Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020.) (Revised by AV, 16-Aug-2024.)

Hypotheses

Ref	Expression
spcedv.1	⊢ (𝜑 → 𝑋 ∈ 𝑉)
spcedv.2	⊢ (𝜑 → 𝜒)
spcedv.3	⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
spcedv	⊢ (𝜑 → ∃𝑥𝜓)

Distinct variable groups:   𝑥,𝑋   𝜒,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem spcedv

Step	Hyp	Ref	Expression
1		spcedv.1	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
2		spcedv.2	. 2 ⊢ (𝜑 → 𝜒)
3		spcedv.3	. . 3 ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))
4	3	spcegv 3610	. 2 ⊢ (𝑋 ∈ 𝑉 → (𝜒 → ∃𝑥𝜓))
5	1, 2, 4	sylc 65	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ∃wex 1777   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-clel 2819

This theorem is referenced by:  selsALT  5459  zfrep6  7995  wfrlem15OLD  8379  ertr  8778  f1dom2gOLD  9030  dom3d  9054  disjenex  9201  domssex2  9203  domssex  9204  brwdom2  9642  infxpenc2lem2  10089  dfac8clem  10101  ac5num  10105  acni2  10115  acnlem  10117  finnisoeu  10182  infpss  10285  cofsmo  10338  axdc4lem  10524  ac6num  10548  axdclem2  10589  hasheqf1od  14402  fz1isolem  14510  wrd2f1tovbij  15009  fsum  15768  ntrivcvgn0  15946  fprod  15989  setsexstruct2  17222  isacs1i  17715  mreacs  17716  gsumval3lem2  19948  eltg3  22990  elptr  23602  nbusgrf1o1  29405  cusgrexg  29479  cusgrfilem3  29493  sizusglecusg  29499  wwlksnextbij  29935  gsumhashmul  33040  fzo0pmtrlast  33085  1arithidom  33530  gblacfnacd  35075  numiunnum  36436  bj-imdirco  37156  eqvreltr  38563  aks6d1c2  42087  sticksstones20  42123  onsucf1lem  43231  onsucf1olem  43232  nnoeomeqom  43274  rp-isfinite5  43479  clrellem  43584  clcnvlem  43585  fundcmpsurinj  47283  prproropen  47382  isuspgrim0  47756  grimidvtxedg  47760  grimcnv  47763  grimco  47764  gricushgr  47770  ushggricedg  47780  uhgrimisgrgric  47783  isgrtri  47794  usgrgrtrirex  47799  uspgrlim  47816  grlimgrtri  47820  grlicref  47829  grlicsym  47830  grlictr  47832  uspgrsprfo  47871  uspgrbispr  47874  1aryenef  48379  2aryenef  48390  eufsnlem  48554  opncldeqv  48581  thincciso  48716  mndtcbas  48754