Theorem spcedv 3561

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 3560	. 2 ⊢ (𝑋 ∈ 𝑉 → (𝜒 → ∃𝑥𝜓))
5	1, 2, 4	sylc 65	1 ⊢ (𝜑 → ∃𝑥𝜓)

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

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 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-clel 2803

This theorem is referenced by:  selsALT  5394  zfrep6  7913  ertr  8663  dom3d  8942  disjenex  9076  domssex2  9078  domssex  9079  brwdom2  9502  infxpenc2lem2  9949  dfac8clem  9961  ac5num  9965  acni2  9975  acnlem  9977  finnisoeu  10042  infpss  10145  cofsmo  10198  axdc4lem  10384  ac6num  10408  axdclem2  10449  hasheqf1od  14294  fz1isolem  14402  wrd2f1tovbij  14902  fsum  15662  ntrivcvgn0  15840  fprod  15883  setsexstruct2  17121  isacs1i  17594  mreacs  17595  gsumval3lem2  19812  eltg3  22825  elptr  23436  nbusgrf1o1  29273  cusgrexg  29347  cusgrfilem3  29361  sizusglecusg  29367  wwlksnextbij  29805  gsumhashmul  32974  fzo0pmtrlast  33022  1arithidom  33481  gblacfnacd  35062  numiunnum  36431  bj-imdirco  37151  eqvreltr  38571  aks6d1c2  42091  sticksstones20  42127  onsucf1lem  43231  onsucf1olem  43232  nnoeomeqom  43274  rp-isfinite5  43479  clrellem  43584  clcnvlem  43585  fundcmpsurinj  47383  prproropen  47482  grimidvtxedg  47858  grimcnv  47861  grimco  47862  isuspgrim0  47867  gricushgr  47890  ushggricedg  47900  uhgrimisgrgric  47904  isgrtri  47915  usgrgrtrirex  47922  isubgr3stgrlem3  47940  isubgr3stgr  47947  uspgrlim  47964  grlimgrtri  47968  grlicref  47977  grlicsym  47978  grlictr  47980  uspgrsprfo  48109  uspgrbispr  48112  1aryenef  48607  2aryenef  48618  eufsnlem  48802  xpco2  48818  opncldeqv  48863  uobffth  49180  uobeqw  49181  thincciso  49415  thinccisod  49416  functermceu  49472  idfudiag1  49487  termcarweu  49490  arweutermc  49492  funcsn  49503  0fucterm  49505  mndtcbas  49543