Theorem spcedv 3564

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 3563	. 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 2708  df-clel 2803

This theorem is referenced by:  selsALT  5399  zfrep6  7933  ertr  8686  dom3d  8965  disjenex  9099  domssex2  9101  domssex  9102  brwdom2  9526  infxpenc2lem2  9973  dfac8clem  9985  ac5num  9989  acni2  9999  acnlem  10001  finnisoeu  10066  infpss  10169  cofsmo  10222  axdc4lem  10408  ac6num  10432  axdclem2  10473  hasheqf1od  14318  fz1isolem  14426  wrd2f1tovbij  14926  fsum  15686  ntrivcvgn0  15864  fprod  15907  setsexstruct2  17145  isacs1i  17618  mreacs  17619  gsumval3lem2  19836  eltg3  22849  elptr  23460  nbusgrf1o1  29297  cusgrexg  29371  cusgrfilem3  29385  sizusglecusg  29391  wwlksnextbij  29832  gsumhashmul  33001  fzo0pmtrlast  33049  1arithidom  33508  gblacfnacd  35089  numiunnum  36458  bj-imdirco  37178  eqvreltr  38598  aks6d1c2  42118  sticksstones20  42154  onsucf1lem  43258  onsucf1olem  43259  nnoeomeqom  43301  rp-isfinite5  43506  clrellem  43611  clcnvlem  43612  fundcmpsurinj  47410  prproropen  47509  grimidvtxedg  47885  grimcnv  47888  grimco  47889  isuspgrim0  47894  gricushgr  47917  ushggricedg  47927  uhgrimisgrgric  47931  isgrtri  47942  usgrgrtrirex  47949  isubgr3stgrlem3  47967  isubgr3stgr  47974  uspgrlim  47991  grlimgrtri  47995  grlicref  48004  grlicsym  48005  grlictr  48007  uspgrsprfo  48136  uspgrbispr  48139  1aryenef  48634  2aryenef  48645  eufsnlem  48829  xpco2  48845  opncldeqv  48890  uobffth  49207  uobeqw  49208  thincciso  49442  thinccisod  49443  functermceu  49499  idfudiag1  49514  termcarweu  49517  arweutermc  49519  funcsn  49530  0fucterm  49532  mndtcbas  49570