Theorem spcedv 3541

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-clel 2812

This theorem is referenced by:  selsALT  5388  zfrep6OLD  7901  ertr  8652  dom3d  8934  disjenex  9066  domssex2  9068  domssex  9069  brwdom2  9481  infxpenc2lem2  9933  dfac8clem  9945  ac5num  9949  acni2  9959  acnlem  9961  finnisoeu  10026  infpss  10129  cofsmo  10182  axdc4lem  10368  ac6num  10392  axdclem2  10433  hasheqf1od  14306  fz1isolem  14414  wrd2f1tovbij  14913  fsum  15673  ntrivcvgn0  15854  fprod  15897  setsexstruct2  17136  isacs1i  17614  mreacs  17615  gsumval3lem2  19872  eltg3  22937  elptr  23548  oldfib  28383  nbusgrf1o1  29453  cusgrexg  29527  cusgrfilem3  29541  sizusglecusg  29547  wwlksnextbij  29985  gsumhashmul  33143  fzo0pmtrlast  33168  1arithidom  33612  fineqvnttrclse  35284  gblacfnacd  35300  numiunnum  36668  bj-imdirco  37520  eqvreltr  39026  aks6d1c2  42583  sticksstones20  42619  onsucf1lem  43715  onsucf1olem  43716  nnoeomeqom  43758  rp-isfinite5  43962  clrellem  44067  clcnvlem  44068  fundcmpsurinj  47881  prproropen  47980  grimidvtxedg  48373  grimcnv  48376  grimco  48377  isuspgrim0  48382  gricushgr  48405  ushggricedg  48415  uhgrimisgrgric  48419  isgrtri  48431  usgrgrtrirex  48438  isubgr3stgrlem3  48456  isubgr3stgr  48463  uspgrlim  48480  grlimgrtri  48491  grlicref  48500  grlicsym  48501  grlictr  48503  uspgrsprfo  48636  uspgrbispr  48639  1aryenef  49133  2aryenef  49144  eufsnlem  49328  xpco2  49344  opncldeqv  49389  uobffth  49705  uobeqw  49706  thincciso  49940  thinccisod  49941  functermceu  49997  idfudiag1  50012  termcarweu  50015  arweutermc  50017  funcsn  50028  0fucterm  50030  mndtcbas  50068