Theorem spcedv 3540

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-clel 2811

This theorem is referenced by:  selsALT  5393  zfrep6OLD  7908  ertr  8659  dom3d  8941  disjenex  9073  domssex2  9075  domssex  9076  brwdom2  9488  infxpenc2lem2  9942  dfac8clem  9954  ac5num  9958  acni2  9968  acnlem  9970  finnisoeu  10035  infpss  10138  cofsmo  10191  axdc4lem  10377  ac6num  10401  axdclem2  10442  hasheqf1od  14315  fz1isolem  14423  wrd2f1tovbij  14922  fsum  15682  ntrivcvgn0  15863  fprod  15906  setsexstruct2  17145  isacs1i  17623  mreacs  17624  gsumval3lem2  19881  eltg3  22927  elptr  23538  oldfib  28369  nbusgrf1o1  29439  cusgrexg  29513  cusgrfilem3  29526  sizusglecusg  29532  wwlksnextbij  29970  gsumhashmul  33128  fzo0pmtrlast  33153  1arithidom  33597  fineqvnttrclse  35268  gblacfnacd  35284  numiunnum  36652  bj-imdirco  37504  eqvreltr  39012  aks6d1c2  42569  sticksstones20  42605  onsucf1lem  43697  onsucf1olem  43698  nnoeomeqom  43740  rp-isfinite5  43944  clrellem  44049  clcnvlem  44050  fundcmpsurinj  47869  prproropen  47968  grimidvtxedg  48361  grimcnv  48364  grimco  48365  isuspgrim0  48370  gricushgr  48393  ushggricedg  48403  uhgrimisgrgric  48407  isgrtri  48419  usgrgrtrirex  48426  isubgr3stgrlem3  48444  isubgr3stgr  48451  uspgrlim  48468  grlimgrtri  48479  grlicref  48488  grlicsym  48489  grlictr  48491  uspgrsprfo  48624  uspgrbispr  48627  1aryenef  49121  2aryenef  49132  eufsnlem  49316  xpco2  49332  opncldeqv  49377  uobffth  49693  uobeqw  49694  thincciso  49928  thinccisod  49929  functermceu  49985  idfudiag1  50000  termcarweu  50003  arweutermc  50005  funcsn  50016  0fucterm  50018  mndtcbas  50056