Theorem spcedv 3552

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ∃wex 1811   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-clel 2835

This theorem is used by:  selsALT  5408  zfrep6OLD  7968  ertr  8737  dom3d  9025  disjenex  9158  domssex2  9160  domssex  9161  brwdom2  9571  infxpenc2lem2  10103  dfac8clem  10115  ac5num  10119  acni2  10129  acnlem  10131  finnisoeu  10196  infpss  10298  cofsmo  10351  axdc4lem  10537  ac6num  10561  axdclem2  10602  hasheqf1od  14501  fz1isolem  14610  wrd2f1tovbij  15119  fsum  15892  ntrivcvgn0  16073  fprod  16114  setsexstruct2  17359  isacs1i  17837  mreacs  17838  gsumval3lem2  20126  eltg3  23286  elptr  23898  oldfib  28769  nbusgrf1o1  29957  cusgrexg  30031  cusgrfilem3  30044  sizusglecusg  30050  wwlksnextbij  30497  gsumhashmul  33675  fzo0pmtrlast  33700  1arithidom  34116  fineqvnttrclse  35849  gblacfnacd  35949  onvfowev  35970  onprcf1of1orbd  35974  mirimanoffr  36547  numiunnum  37351  bj-imdirco  38205  eqvreltr  39717  aks6d1c2  43274  sticksstones20  43310  onsucf1lem  44365  onsucf1olem  44366  nnoeomeqom  44408  rp-isfinite5  44612  clrellem  44716  clcnvlem  44717  fundcmpsurinj  48585  prproropen  48684  grimidvtxedg  49077  grimcnv  49080  grimco  49081  isuspgrim0  49086  gricushgr  49109  ushggricedg  49119  uhgrimisgrgric  49123  isgrtri  49135  usgrgrtrirex  49142  isubgr3stgrlem3  49160  isubgr3stgr  49167  uspgrlim  49184  grlimgrtri  49195  grlicref  49204  grlicsym  49205  grlictr  49207  uspgrsprfo  49340  uspgrbispr  49343  1aryenef  49851  2aryenef  49862  eufsnlem  50046  xpco2  50062  opncldbid  50110  uobffth  50428  uobeqw  50429  thincciso  50682  thinccisod  50683  functermceu  50739  idfudiag1  50754  termcarweu  50757  arweutermc  50759  funcsn  50773  0fucterm  50775  mndtcbaseu  50813