Theorem spcedv 3535

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ∃wex 1785   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-clel 2817

This theorem is referenced by:  zfrep6  7784  wfrlem15OLD  8138  ertr  8487  f1dom2gOLD  8729  dom3d  8753  disjenex  8887  domssex2  8889  domssex  8890  brwdom2  9293  infxpenc2lem2  9760  dfac8clem  9772  ac5num  9776  acni2  9786  acnlem  9788  finnisoeu  9853  infpss  9957  cofsmo  10009  axdc4lem  10195  ac6num  10219  axdclem2  10260  hasheqf1od  14049  fz1isolem  14156  wrd2f1tovbij  14656  fsum  15413  ntrivcvgn0  15591  fprod  15632  setsexstruct2  16857  isacs1i  17347  mreacs  17348  gsumval3lem2  19488  eltg3  22093  elptr  22705  nbusgrf1o1  27718  cusgrexg  27792  cusgrfilem3  27805  sizusglecusg  27811  wwlksnextbij  28246  gsumhashmul  31295  bj-imdirco  35340  eqvreltr  36699  sticksstones20  40102  clrellem  41183  clcnvlem  41184  fundcmpsurinj  44813  prproropen  44912  isomgreqve  45229  isomushgr  45230  isomgrsym  45240  isomgrtr  45243  ushrisomgr  45245  uspgrsprfo  45262  uspgrbispr  45265  1aryenef  45943  2aryenef  45954  eufsnlem  46120  opncldeqv  46147  thincciso  46282  mndtcbas  46320