Theorem spcedv 3553

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

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

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 2147

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

This theorem is used by:  selsALT  5409  zfrep6OLD  7965  ertr  8726  dom3d  9014  disjenex  9147  domssex2  9149  domssex  9150  brwdom2  9560  infxpenc2lem2  10092  dfac8clem  10104  ac5num  10108  acni2  10118  acnlem  10120  finnisoeu  10185  infpss  10287  cofsmo  10340  axdc4lem  10526  ac6num  10550  axdclem2  10591  hasheqf1od  14490  fz1isolem  14599  wrd2f1tovbij  15106  fsum  15879  ntrivcvgn0  16060  fprod  16101  setsexstruct2  17346  isacs1i  17824  mreacs  17825  gsumval3lem2  20113  eltg3  23273  elptr  23885  oldfib  28756  nbusgrf1o1  29944  cusgrexg  30018  cusgrfilem3  30031  sizusglecusg  30037  wwlksnextbij  30484  gsumhashmul  33621  fzo0pmtrlast  33646  1arithidom  34062  fineqvnttrclse  35775  gblacfnacd  35864  onvfowev  35878  numiunnum  37238  bj-imdirco  38091  eqvreltr  39603  aks6d1c2  43160  sticksstones20  43196  onsucf1lem  44255  onsucf1olem  44256  nnoeomeqom  44298  rp-isfinite5  44502  clrellem  44607  clcnvlem  44608  fundcmpsurinj  48460  prproropen  48559  grimidvtxedg  48952  grimcnv  48955  grimco  48956  isuspgrim0  48961  gricushgr  48984  ushggricedg  48994  uhgrimisgrgric  48998  isgrtri  49010  usgrgrtrirex  49017  isubgr3stgrlem3  49035  isubgr3stgr  49042  uspgrlim  49059  grlimgrtri  49070  grlicref  49079  grlicsym  49080  grlictr  49082  uspgrsprfo  49215  uspgrbispr  49218  1aryenef  49726  2aryenef  49737  eufsnlem  49920  xpco2  49936  opncldbid  49979  uobffth  50295  uobeqw  50296  thincciso  50530  thinccisod  50531  functermceu  50587  idfudiag1  50602  termcarweu  50605  arweutermc  50607  funcsn  50618  0fucterm  50620  mndtcbaseu  50658