Theorem spcedv 3589

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ∃wex 1782   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-clel 2811

This theorem is referenced by:  selsALT  5440  zfrep6  7941  wfrlem15OLD  8323  ertr  8718  f1dom2gOLD  8966  dom3d  8990  disjenex  9135  domssex2  9137  domssex  9138  brwdom2  9568  infxpenc2lem2  10015  dfac8clem  10027  ac5num  10031  acni2  10041  acnlem  10043  finnisoeu  10108  infpss  10212  cofsmo  10264  axdc4lem  10450  ac6num  10474  axdclem2  10515  hasheqf1od  14313  fz1isolem  14422  wrd2f1tovbij  14911  fsum  15666  ntrivcvgn0  15844  fprod  15885  setsexstruct2  17108  isacs1i  17601  mreacs  17602  gsumval3lem2  19774  eltg3  22465  elptr  23077  nbusgrf1o1  28627  cusgrexg  28701  cusgrfilem3  28714  sizusglecusg  28720  wwlksnextbij  29156  gsumhashmul  32208  bj-imdirco  36071  eqvreltr  37477  sticksstones20  40982  onsucf1lem  42019  onsucf1olem  42020  nnoeomeqom  42062  rp-isfinite5  42268  clrellem  42373  clcnvlem  42374  fundcmpsurinj  46077  prproropen  46176  isomgreqve  46493  isomushgr  46494  isomgrsym  46504  isomgrtr  46507  ushrisomgr  46509  uspgrsprfo  46526  uspgrbispr  46529  1aryenef  47331  2aryenef  47342  eufsnlem  47507  opncldeqv  47534  thincciso  47669  mndtcbas  47707