Theorem spcedv 3598

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-clel 2814

This theorem is referenced by:  selsALT  5450  zfrep6  7978  wfrlem15OLD  8362  ertr  8759  dom3d  9033  disjenex  9174  domssex2  9176  domssex  9177  brwdom2  9611  infxpenc2lem2  10058  dfac8clem  10070  ac5num  10074  acni2  10084  acnlem  10086  finnisoeu  10151  infpss  10254  cofsmo  10307  axdc4lem  10493  ac6num  10517  axdclem2  10558  hasheqf1od  14389  fz1isolem  14497  wrd2f1tovbij  14996  fsum  15753  ntrivcvgn0  15931  fprod  15974  setsexstruct2  17209  isacs1i  17702  mreacs  17703  gsumval3lem2  19939  eltg3  22985  elptr  23597  nbusgrf1o1  29402  cusgrexg  29476  cusgrfilem3  29490  sizusglecusg  29496  wwlksnextbij  29932  gsumhashmul  33047  fzo0pmtrlast  33095  1arithidom  33545  gblacfnacd  35092  numiunnum  36453  bj-imdirco  37173  eqvreltr  38589  aks6d1c2  42112  sticksstones20  42148  onsucf1lem  43259  onsucf1olem  43260  nnoeomeqom  43302  rp-isfinite5  43507  clrellem  43612  clcnvlem  43613  fundcmpsurinj  47334  prproropen  47433  isuspgrim0  47810  grimidvtxedg  47814  grimcnv  47817  grimco  47818  gricushgr  47824  ushggricedg  47834  uhgrimisgrgric  47837  isgrtri  47848  usgrgrtrirex  47853  isubgr3stgrlem3  47871  isubgr3stgr  47878  uspgrlim  47895  grlimgrtri  47899  grlicref  47908  grlicsym  47909  grlictr  47911  uspgrsprfo  47992  uspgrbispr  47995  1aryenef  48495  2aryenef  48506  eufsnlem  48671  opncldeqv  48698  thincciso  48849  thinccisod  48850  mndtcbas  48890