Theorem spcedv 3598

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

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

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 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-clel 2816

This theorem is referenced by:  selsALT  5444  zfrep6  7979  wfrlem15OLD  8363  ertr  8760  dom3d  9034  disjenex  9175  domssex2  9177  domssex  9178  brwdom2  9613  infxpenc2lem2  10060  dfac8clem  10072  ac5num  10076  acni2  10086  acnlem  10088  finnisoeu  10153  infpss  10256  cofsmo  10309  axdc4lem  10495  ac6num  10519  axdclem2  10560  hasheqf1od  14392  fz1isolem  14500  wrd2f1tovbij  14999  fsum  15756  ntrivcvgn0  15934  fprod  15977  setsexstruct2  17212  isacs1i  17700  mreacs  17701  gsumval3lem2  19924  eltg3  22969  elptr  23581  nbusgrf1o1  29387  cusgrexg  29461  cusgrfilem3  29475  sizusglecusg  29481  wwlksnextbij  29922  gsumhashmul  33064  fzo0pmtrlast  33112  1arithidom  33565  gblacfnacd  35113  numiunnum  36471  bj-imdirco  37191  eqvreltr  38608  aks6d1c2  42131  sticksstones20  42167  onsucf1lem  43282  onsucf1olem  43283  nnoeomeqom  43325  rp-isfinite5  43530  clrellem  43635  clcnvlem  43636  fundcmpsurinj  47396  prproropen  47495  isuspgrim0  47872  grimidvtxedg  47876  grimcnv  47879  grimco  47880  gricushgr  47886  ushggricedg  47896  uhgrimisgrgric  47899  isgrtri  47910  usgrgrtrirex  47917  isubgr3stgrlem3  47935  isubgr3stgr  47942  uspgrlim  47959  grlimgrtri  47963  grlicref  47972  grlicsym  47973  grlictr  47975  uspgrsprfo  48064  uspgrbispr  48067  1aryenef  48566  2aryenef  48577  eufsnlem  48750  opncldeqv  48799  thincciso  49102  thinccisod  49103  functermceu  49142  mndtcbas  49178