Theorem spcedv 3547

Description: Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020.)

Hypotheses

Ref	Expression
spcedv.1	⊢ (𝜑 → 𝑋 ∈ V)
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 ⊢ (𝜑 → 𝑋 ∈ V)
2		spcedv.2	. 2 ⊢ (𝜑 → 𝜒)
3		spcedv.3	. . 3 ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))
4	3	spcegv 3545	. 2 ⊢ (𝑋 ∈ V → (𝜒 → ∃𝑥𝜓))
5	1, 2, 4	sylc 65	1 ⊢ (𝜑 → ∃𝑥𝜓)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ∃wex 1781   ∈ wcel 2111  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  zfrep6  7638  wfrlem15  7952  ertr  8287  f1dom2g  8510  dom3d  8534  disjenex  8659  domssex2  8661  domssex  8662  brwdom2  9021  infxpenc2lem2  9431  dfac8clem  9443  ac5num  9447  acni2  9457  acnlem  9459  finnisoeu  9524  infpss  9628  cofsmo  9680  axdc4lem  9866  ac6num  9890  axdclem2  9931  hasheqf1od  13710  fz1isolem  13815  wrd2f1tovbij  14315  fsum  15069  ntrivcvgn0  15246  fprod  15287  setsexstruct2  16514  isacs1i  16920  mreacs  16921  gsumval3lem2  19019  eltg3  21567  elptr  22178  nbusgrf1o1  27160  cusgrexg  27234  cusgrfilem3  27247  sizusglecusg  27253  wwlksnextbij  27688  gsumhashmul  30741  bj-imdirco  34605  eqvreltr  36002  clrellem  40322  clcnvlem  40323  fundcmpsurinj  43926  prproropen  44025  isomgreqve  44343  isomushgr  44344  isomgrsym  44354  isomgrtr  44357  ushrisomgr  44359  uspgrsprfo  44376  uspgrbispr  44379  1aryenef  45059  2aryenef  45070