Theorem spcedv 3555

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 3554	. 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  5386  zfrep6  7897  ertr  8647  dom3d  8926  disjenex  9059  domssex2  9061  domssex  9062  brwdom2  9484  infxpenc2lem2  9933  dfac8clem  9945  ac5num  9949  acni2  9959  acnlem  9961  finnisoeu  10026  infpss  10129  cofsmo  10182  axdc4lem  10368  ac6num  10392  axdclem2  10433  hasheqf1od  14278  fz1isolem  14386  wrd2f1tovbij  14885  fsum  15645  ntrivcvgn0  15823  fprod  15866  setsexstruct2  17104  isacs1i  17581  mreacs  17582  gsumval3lem2  19803  eltg3  22865  elptr  23476  nbusgrf1o1  29333  cusgrexg  29407  cusgrfilem3  29421  sizusglecusg  29427  wwlksnextbij  29865  gsumhashmul  33027  fzo0pmtrlast  33047  1arithidom  33487  gblacfnacd  35077  numiunnum  36446  bj-imdirco  37166  eqvreltr  38586  aks6d1c2  42106  sticksstones20  42142  onsucf1lem  43245  onsucf1olem  43246  nnoeomeqom  43288  rp-isfinite5  43493  clrellem  43598  clcnvlem  43599  fundcmpsurinj  47397  prproropen  47496  grimidvtxedg  47873  grimcnv  47876  grimco  47877  isuspgrim0  47882  gricushgr  47905  ushggricedg  47915  uhgrimisgrgric  47919  isgrtri  47931  usgrgrtrirex  47938  isubgr3stgrlem3  47956  isubgr3stgr  47963  uspgrlim  47980  grlimgrtri  47991  grlicref  48000  grlicsym  48001  grlictr  48003  uspgrsprfo  48136  uspgrbispr  48139  1aryenef  48634  2aryenef  48645  eufsnlem  48829  xpco2  48845  opncldeqv  48890  uobffth  49207  uobeqw  49208  thincciso  49442  thinccisod  49443  functermceu  49499  idfudiag1  49514  termcarweu  49517  arweutermc  49519  funcsn  49530  0fucterm  49532  mndtcbas  49570