Theorem spcedv 3556

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  ∃wex 1798   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-clel 2836

This theorem is referenced by:  selsALT  5405  zfrep6OLD  7931  ertr  8688  dom3d  8969  disjenex  9101  domssex2  9103  domssex  9104  brwdom2  9515  infxpenc2lem2  9970  dfac8clem  9982  ac5num  9986  acni2  9996  acnlem  9998  finnisoeu  10063  infpss  10166  cofsmo  10220  axdc4lem  10406  ac6num  10430  axdclem2  10471  hasheqf1od  14360  fz1isolem  14468  wrd2f1tovbij  14967  fsum  15738  ntrivcvgn0  15919  fprod  15962  setsexstruct2  17202  isacs1i  17680  mreacs  17681  gsumval3lem2  19937  eltg3  23010  elptr  23621  oldfib  28458  nbusgrf1o1  29528  cusgrexg  29602  cusgrfilem3  29615  sizusglecusg  29621  wwlksnextbij  30059  gsumhashmul  33208  fzo0pmtrlast  33233  1arithidom  33694  fineqvnttrclse  35381  gblacfnacd  35406  onvfowev  35420  numiunnum  36791  bj-imdirco  37643  eqvreltr  39151  aks6d1c2  42708  sticksstones20  42744  onsucf1lem  43807  onsucf1olem  43808  nnoeomeqom  43850  rp-isfinite5  44054  clrellem  44159  clcnvlem  44160  fundcmpsurinj  47976  prproropen  48075  grimidvtxedg  48468  grimcnv  48471  grimco  48472  isuspgrim0  48477  gricushgr  48500  ushggricedg  48510  uhgrimisgrgric  48514  isgrtri  48526  usgrgrtrirex  48533  isubgr3stgrlem3  48551  isubgr3stgr  48558  uspgrlim  48575  grlimgrtri  48586  grlicref  48595  grlicsym  48596  grlictr  48598  uspgrsprfo  48731  uspgrbispr  48734  1aryenef  49228  2aryenef  49239  eufsnlem  49423  xpco2  49439  opncldeqv  49484  uobffth  49800  uobeqw  49801  thincciso  50035  thinccisod  50036  functermceu  50092  idfudiag1  50107  termcarweu  50110  arweutermc  50112  funcsn  50123  0fucterm  50125  mndtcbas  50163