Theorem spcedv 3588

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  ∃wex 1780   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-clel 2809

This theorem is referenced by:  selsALT  5439  zfrep6  7945  wfrlem15OLD  8329  ertr  8724  f1dom2gOLD  8972  dom3d  8996  disjenex  9141  domssex2  9143  domssex  9144  brwdom2  9574  infxpenc2lem2  10021  dfac8clem  10033  ac5num  10037  acni2  10047  acnlem  10049  finnisoeu  10114  infpss  10218  cofsmo  10270  axdc4lem  10456  ac6num  10480  axdclem2  10521  hasheqf1od  14320  fz1isolem  14429  wrd2f1tovbij  14918  fsum  15673  ntrivcvgn0  15851  fprod  15892  setsexstruct2  17115  isacs1i  17608  mreacs  17609  gsumval3lem2  19822  eltg3  22785  elptr  23397  nbusgrf1o1  29060  cusgrexg  29134  cusgrfilem3  29147  sizusglecusg  29153  wwlksnextbij  29589  gsumhashmul  32644  bj-imdirco  36535  eqvreltr  37941  sticksstones20  41449  onsucf1lem  42482  onsucf1olem  42483  nnoeomeqom  42525  rp-isfinite5  42731  clrellem  42836  clcnvlem  42837  fundcmpsurinj  46536  prproropen  46635  isomgreqve  46952  isomushgr  46953  isomgrsym  46963  isomgrtr  46966  ushrisomgr  46968  uspgrsprfo  46985  uspgrbispr  46988  1aryenef  47493  2aryenef  47504  eufsnlem  47669  opncldeqv  47696  thincciso  47831  mndtcbas  47869