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 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 2739  df-clel 2835

This theorem is used by:  selsALT  5416  zfrep6OLD  7952  ertr  8712  dom3d  9000  disjenex  9133  domssex2  9135  domssex  9136  brwdom2  9545  infxpenc2lem2  10023  dfac8clem  10035  ac5num  10039  acni2  10049  acnlem  10051  finnisoeu  10116  infpss  10218  cofsmo  10271  axdc4lem  10457  ac6num  10481  axdclem2  10522  hasheqf1od  14417  fz1isolem  14526  wrd2f1tovbij  15033  fsum  15806  ntrivcvgn0  15987  fprod  16028  setsexstruct2  17267  isacs1i  17745  mreacs  17746  gsumval3lem2  20033  eltg3  23187  elptr  23799  oldfib  28642  nbusgrf1o1  29830  cusgrexg  29904  cusgrfilem3  29917  sizusglecusg  29923  wwlksnextbij  30370  gsumhashmul  33507  fzo0pmtrlast  33532  1arithidom  33947  fineqvnttrclse  35650  gblacfnacd  35699  onvfowev  35713  numiunnum  37089  bj-imdirco  37942  eqvreltr  39439  aks6d1c2  42996  sticksstones20  43032  onsucf1lem  44110  onsucf1olem  44111  nnoeomeqom  44153  rp-isfinite5  44357  clrellem  44462  clcnvlem  44463  fundcmpsurinj  48309  prproropen  48408  grimidvtxedg  48801  grimcnv  48804  grimco  48805  isuspgrim0  48810  gricushgr  48833  ushggricedg  48843  uhgrimisgrgric  48847  isgrtri  48859  usgrgrtrirex  48866  isubgr3stgrlem3  48884  isubgr3stgr  48891  uspgrlim  48908  grlimgrtri  48919  grlicref  48928  grlicsym  48929  grlictr  48931  uspgrsprfo  49064  uspgrbispr  49067  1aryenef  49575  2aryenef  49586  eufsnlem  49769  xpco2  49785  opncldeqv  49828  uobffth  50144  uobeqw  50145  thincciso  50379  thinccisod  50380  functermceu  50436  idfudiag1  50451  termcarweu  50454  arweutermc  50456  funcsn  50467  0fucterm  50469  mndtcbas  50507