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  28658  cusgrexg  28732  cusgrfilem3  28745  sizusglecusg  28751  wwlksnextbij  29187  gsumhashmul  32239  bj-imdirco  36119  eqvreltr  37525  sticksstones20  41030  onsucf1lem  42067  onsucf1olem  42068  nnoeomeqom  42110  rp-isfinite5  42316  clrellem  42421  clcnvlem  42422  fundcmpsurinj  46125  prproropen  46224  isomgreqve  46541  isomushgr  46542  isomgrsym  46552  isomgrtr  46555  ushrisomgr  46557  uspgrsprfo  46574  uspgrbispr  46577  1aryenef  47379  2aryenef  47390  eufsnlem  47555  opncldeqv  47582  thincciso  47717  mndtcbas  47755