Theorem spcedv 3559

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-clel 2840

This theorem is used by:  selsALT  5424  zfrep6OLD  7954  ertr  8712  dom3d  8993  disjenex  9126  domssex2  9128  domssex  9129  brwdom2  9538  infxpenc2lem2  10016  dfac8clem  10028  ac5num  10032  acni2  10042  acnlem  10044  finnisoeu  10109  infpss  10211  cofsmo  10264  axdc4lem  10450  ac6num  10474  axdclem2  10515  hasheqf1od  14402  fz1isolem  14511  wrd2f1tovbij  15016  fsum  15789  ntrivcvgn0  15970  fprod  16013  setsexstruct2  17252  isacs1i  17730  mreacs  17731  gsumval3lem2  19999  eltg3  23148  elptr  23759  oldfib  28599  nbusgrf1o1  29749  cusgrexg  29823  cusgrfilem3  29836  sizusglecusg  29842  wwlksnextbij  30280  gsumhashmul  33410  fzo0pmtrlast  33435  1arithidom  33850  fineqvnttrclse  35553  gblacfnacd  35602  onvfowev  35616  numiunnum  37014  bj-imdirco  37867  eqvreltr  39373  aks6d1c2  42930  sticksstones20  42966  onsucf1lem  44029  onsucf1olem  44030  nnoeomeqom  44072  rp-isfinite5  44276  clrellem  44381  clcnvlem  44382  fundcmpsurinj  48191  prproropen  48290  grimidvtxedg  48683  grimcnv  48686  grimco  48687  isuspgrim0  48692  gricushgr  48715  ushggricedg  48725  uhgrimisgrgric  48729  isgrtri  48741  usgrgrtrirex  48748  isubgr3stgrlem3  48766  isubgr3stgr  48773  uspgrlim  48790  grlimgrtri  48801  grlicref  48810  grlicsym  48811  grlictr  48813  uspgrsprfo  48946  uspgrbispr  48949  1aryenef  49458  2aryenef  49469  eufsnlem  49652  xpco2  49668  opncldeqv  49713  uobffth  50029  uobeqw  50030  thincciso  50264  thinccisod  50265  functermceu  50321  idfudiag1  50336  termcarweu  50339  arweutermc  50341  funcsn  50352  0fucterm  50354  mndtcbas  50392