Theorem spcedv 3552

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2113

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 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-clel 2811

This theorem is referenced by:  selsALT  5389  zfrep6  7899  ertr  8650  dom3d  8931  disjenex  9063  domssex2  9065  domssex  9066  brwdom2  9478  infxpenc2lem2  9930  dfac8clem  9942  ac5num  9946  acni2  9956  acnlem  9958  finnisoeu  10023  infpss  10126  cofsmo  10179  axdc4lem  10365  ac6num  10389  axdclem2  10430  hasheqf1od  14276  fz1isolem  14384  wrd2f1tovbij  14883  fsum  15643  ntrivcvgn0  15821  fprod  15864  setsexstruct2  17102  isacs1i  17580  mreacs  17581  gsumval3lem2  19835  eltg3  22906  elptr  23517  oldfib  28373  nbusgrf1o1  29443  cusgrexg  29517  cusgrfilem3  29531  sizusglecusg  29537  wwlksnextbij  29975  gsumhashmul  33150  fzo0pmtrlast  33174  1arithidom  33618  fineqvnttrclse  35280  gblacfnacd  35296  numiunnum  36664  bj-imdirco  37395  eqvreltr  38864  aks6d1c2  42384  sticksstones20  42420  onsucf1lem  43511  onsucf1olem  43512  nnoeomeqom  43554  rp-isfinite5  43758  clrellem  43863  clcnvlem  43864  fundcmpsurinj  47655  prproropen  47754  grimidvtxedg  48131  grimcnv  48134  grimco  48135  isuspgrim0  48140  gricushgr  48163  ushggricedg  48173  uhgrimisgrgric  48177  isgrtri  48189  usgrgrtrirex  48196  isubgr3stgrlem3  48214  isubgr3stgr  48221  uspgrlim  48238  grlimgrtri  48249  grlicref  48258  grlicsym  48259  grlictr  48261  uspgrsprfo  48394  uspgrbispr  48397  1aryenef  48891  2aryenef  48902  eufsnlem  49086  xpco2  49102  opncldeqv  49147  uobffth  49463  uobeqw  49464  thincciso  49698  thinccisod  49699  functermceu  49755  idfudiag1  49770  termcarweu  49773  arweutermc  49775  funcsn  49786  0fucterm  49788  mndtcbas  49826