Theorem spcedv 3543

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ∃wex 1786   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-clel 2815

This theorem is referenced by:  selsALT  5387  zfrep6OLD  7904  ertr  8656  dom3d  8938  disjenex  9070  domssex2  9072  domssex  9073  brwdom2  9485  infxpenc2lem2  9940  dfac8clem  9952  ac5num  9956  acni2  9966  acnlem  9968  finnisoeu  10033  infpss  10136  cofsmo  10189  axdc4lem  10375  ac6num  10399  axdclem2  10440  hasheqf1od  14313  fz1isolem  14421  wrd2f1tovbij  14920  fsum  15680  ntrivcvgn0  15861  fprod  15904  setsexstruct2  17143  isacs1i  17621  mreacs  17622  gsumval3lem2  19879  eltg3  22952  elptr  23563  oldfib  28394  nbusgrf1o1  29464  cusgrexg  29538  cusgrfilem3  29551  sizusglecusg  29557  wwlksnextbij  29995  gsumhashmul  33155  fzo0pmtrlast  33180  1arithidom  33627  fineqvnttrclse  35312  gblacfnacd  35337  numiunnum  36705  bj-imdirco  37557  eqvreltr  39065  aks6d1c2  42622  sticksstones20  42658  onsucf1lem  43721  onsucf1olem  43722  nnoeomeqom  43764  rp-isfinite5  43968  clrellem  44073  clcnvlem  44074  fundcmpsurinj  47891  prproropen  47990  grimidvtxedg  48383  grimcnv  48386  grimco  48387  isuspgrim0  48392  gricushgr  48415  ushggricedg  48425  uhgrimisgrgric  48429  isgrtri  48441  usgrgrtrirex  48448  isubgr3stgrlem3  48466  isubgr3stgr  48473  uspgrlim  48490  grlimgrtri  48501  grlicref  48510  grlicsym  48511  grlictr  48513  uspgrsprfo  48646  uspgrbispr  48649  1aryenef  49143  2aryenef  49154  eufsnlem  49338  xpco2  49354  opncldeqv  49399  uobffth  49715  uobeqw  49716  thincciso  49950  thinccisod  49951  functermceu  50007  idfudiag1  50022  termcarweu  50025  arweutermc  50027  funcsn  50038  0fucterm  50040  mndtcbas  50078