Theorem spcedv 3556

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-clel 2839

This theorem is used by:  selsALT  5416  zfrep6OLD  8001  ertr  8771  dom3d  9059  disjenex  9192  domssex2  9194  domssex  9195  brwdom2  9604  infxpenc2lem2  10138  dfac8clem  10150  ac5num  10154  acni2  10164  acnlem  10166  finnisoeu  10231  infpss  10333  cofsmo  10386  axdc4lem  10572  ac6num  10596  axdclem2  10637  hasheqf1od  14538  fz1isolem  14647  wrd2f1tovbij  15156  fsum  15930  ntrivcvgn0  16111  fprod  16152  setsexstruct2  17397  isacs1i  17881  mreacs  17882  gsumval3lem2  20171  eltg3  23335  elptr  23947  oldfib  28820  nbusgrf1o1  30008  cusgrexg  30082  cusgrfilem3  30095  sizusglecusg  30101  wwlksnextbij  30548  gsumhashmul  33727  fzo0pmtrlast  33752  1arithidom  34173  fineqvnttrclse  35933  gblacfnacd  36070  onvfowev  36091  onprcf1of1orbd  36095  mirimanoffr  36668  elpssmo  36673  numiunnum  37473  bj-imdirco  38379  eqvreltr  39889  aks6d1c2  43446  sticksstones20  43482  onsucf1lem  44532  onsucf1olem  44533  nnoeomeqom  44575  rp-isfinite5  44779  clrellem  44883  clcnvlem  44884  fundcmpsurinj  48764  prproropen  48863  grimidvtxedg  49256  grimcnv  49259  grimco  49260  isuspgrim0  49265  gricushgr  49288  ushggricedg  49298  uhgrimisgrgric  49302  isgrtri  49314  usgrgrtrirex  49321  isubgr3stgrlem3  49339  isubgr3stgr  49346  uspgrlim  49363  grlimgrtri  49374  grlicref  49383  grlicsym  49384  grlictr  49386  uspgrsprfo  49519  uspgrbispr  49522  1aryenef  50088  2aryenef  50099  eufsnlem  50283  xpco2  50299  opncldbid  50347  uobffth  50665  uobeqw  50666  thincciso  50919  thinccisod  50920  functermceu  50976  idfudiag1  50991  termcarweu  50994  arweutermc  50996  funcsn  51010  0fucterm  51012  mndtcbaseu  51050