Theorem spcedv 3554

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 3553	. 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 2716  df-clel 2812

This theorem is referenced by:  selsALT  5396  zfrep6  7909  ertr  8661  dom3d  8943  disjenex  9075  domssex2  9077  domssex  9078  brwdom2  9490  infxpenc2lem2  9942  dfac8clem  9954  ac5num  9958  acni2  9968  acnlem  9970  finnisoeu  10035  infpss  10138  cofsmo  10191  axdc4lem  10377  ac6num  10401  axdclem2  10442  hasheqf1od  14288  fz1isolem  14396  wrd2f1tovbij  14895  fsum  15655  ntrivcvgn0  15833  fprod  15876  setsexstruct2  17114  isacs1i  17592  mreacs  17593  gsumval3lem2  19847  eltg3  22918  elptr  23529  oldfib  28385  nbusgrf1o1  29455  cusgrexg  29529  cusgrfilem3  29543  sizusglecusg  29549  wwlksnextbij  29987  gsumhashmul  33160  fzo0pmtrlast  33185  1arithidom  33629  fineqvnttrclse  35299  gblacfnacd  35315  numiunnum  36683  bj-imdirco  37442  eqvreltr  38939  aks6d1c2  42497  sticksstones20  42533  onsucf1lem  43623  onsucf1olem  43624  nnoeomeqom  43666  rp-isfinite5  43870  clrellem  43975  clcnvlem  43976  fundcmpsurinj  47766  prproropen  47865  grimidvtxedg  48242  grimcnv  48245  grimco  48246  isuspgrim0  48251  gricushgr  48274  ushggricedg  48284  uhgrimisgrgric  48288  isgrtri  48300  usgrgrtrirex  48307  isubgr3stgrlem3  48325  isubgr3stgr  48332  uspgrlim  48349  grlimgrtri  48360  grlicref  48369  grlicsym  48370  grlictr  48372  uspgrsprfo  48505  uspgrbispr  48508  1aryenef  49002  2aryenef  49013  eufsnlem  49197  xpco2  49213  opncldeqv  49258  uobffth  49574  uobeqw  49575  thincciso  49809  thinccisod  49810  functermceu  49866  idfudiag1  49881  termcarweu  49884  arweutermc  49886  funcsn  49897  0fucterm  49899  mndtcbas  49937