Theorem spcedv 3558

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ∃wex 1809   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-clel 2838

This theorem is referenced by:  selsALT  5424  zfrep6OLD  7953  ertr  8711  dom3d  8992  disjenex  9124  domssex2  9126  domssex  9127  brwdom2  9536  infxpenc2lem2  10005  dfac8clem  10017  ac5num  10021  acni2  10031  acnlem  10033  finnisoeu  10098  infpss  10200  cofsmo  10254  axdc4lem  10440  ac6num  10464  axdclem2  10505  hasheqf1od  14391  fz1isolem  14500  wrd2f1tovbij  14999  fsum  15773  ntrivcvgn0  15954  fprod  15997  setsexstruct2  17236  isacs1i  17714  mreacs  17715  gsumval3lem2  19977  eltg3  23100  elptr  23711  oldfib  28551  nbusgrf1o1  29701  cusgrexg  29775  cusgrfilem3  29788  sizusglecusg  29794  wwlksnextbij  30232  gsumhashmul  33368  fzo0pmtrlast  33393  1arithidom  33808  fineqvnttrclse  35518  gblacfnacd  35567  onvfowev  35581  numiunnum  36962  bj-imdirco  37815  eqvreltr  39321  aks6d1c2  42878  sticksstones20  42914  onsucf1lem  43979  onsucf1olem  43980  nnoeomeqom  44022  rp-isfinite5  44226  clrellem  44331  clcnvlem  44332  fundcmpsurinj  48141  prproropen  48240  grimidvtxedg  48633  grimcnv  48636  grimco  48637  isuspgrim0  48642  gricushgr  48665  ushggricedg  48675  uhgrimisgrgric  48679  isgrtri  48691  usgrgrtrirex  48698  isubgr3stgrlem3  48716  isubgr3stgr  48723  uspgrlim  48740  grlimgrtri  48751  grlicref  48760  grlicsym  48761  grlictr  48763  uspgrsprfo  48896  uspgrbispr  48899  1aryenef  49408  2aryenef  49419  eufsnlem  49602  xpco2  49618  opncldeqv  49663  uobffth  49979  uobeqw  49980  thincciso  50214  thinccisod  50215  functermceu  50271  idfudiag1  50286  termcarweu  50289  arweutermc  50291  funcsn  50302  0fucterm  50304  mndtcbas  50342