Theorem spcedv 3567

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-clel 2804

This theorem is referenced by:  selsALT  5402  zfrep6  7936  ertr  8689  dom3d  8968  disjenex  9105  domssex2  9107  domssex  9108  brwdom2  9533  infxpenc2lem2  9980  dfac8clem  9992  ac5num  9996  acni2  10006  acnlem  10008  finnisoeu  10073  infpss  10176  cofsmo  10229  axdc4lem  10415  ac6num  10439  axdclem2  10480  hasheqf1od  14325  fz1isolem  14433  wrd2f1tovbij  14933  fsum  15693  ntrivcvgn0  15871  fprod  15914  setsexstruct2  17152  isacs1i  17625  mreacs  17626  gsumval3lem2  19843  eltg3  22856  elptr  23467  nbusgrf1o1  29304  cusgrexg  29378  cusgrfilem3  29392  sizusglecusg  29398  wwlksnextbij  29839  gsumhashmul  33008  fzo0pmtrlast  33056  1arithidom  33515  gblacfnacd  35096  numiunnum  36465  bj-imdirco  37185  eqvreltr  38605  aks6d1c2  42125  sticksstones20  42161  onsucf1lem  43265  onsucf1olem  43266  nnoeomeqom  43308  rp-isfinite5  43513  clrellem  43618  clcnvlem  43619  fundcmpsurinj  47414  prproropen  47513  grimidvtxedg  47889  grimcnv  47892  grimco  47893  isuspgrim0  47898  gricushgr  47921  ushggricedg  47931  uhgrimisgrgric  47935  isgrtri  47946  usgrgrtrirex  47953  isubgr3stgrlem3  47971  isubgr3stgr  47978  uspgrlim  47995  grlimgrtri  47999  grlicref  48008  grlicsym  48009  grlictr  48011  uspgrsprfo  48140  uspgrbispr  48143  1aryenef  48638  2aryenef  48649  eufsnlem  48833  xpco2  48849  opncldeqv  48894  uobffth  49211  uobeqw  49212  thincciso  49446  thinccisod  49447  functermceu  49503  idfudiag1  49518  termcarweu  49521  arweutermc  49523  funcsn  49534  0fucterm  49536  mndtcbas  49574