Theorem spcedv 3581

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539  ∃wex 1778   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-clel 2808

This theorem is referenced by:  selsALT  5424  zfrep6  7961  wfrlem15OLD  8345  ertr  8742  dom3d  9016  disjenex  9157  domssex2  9159  domssex  9160  brwdom2  9595  infxpenc2lem2  10042  dfac8clem  10054  ac5num  10058  acni2  10068  acnlem  10070  finnisoeu  10135  infpss  10238  cofsmo  10291  axdc4lem  10477  ac6num  10501  axdclem2  10542  hasheqf1od  14375  fz1isolem  14483  wrd2f1tovbij  14982  fsum  15739  ntrivcvgn0  15917  fprod  15960  setsexstruct2  17195  isacs1i  17672  mreacs  17673  gsumval3lem2  19893  eltg3  22917  elptr  23528  nbusgrf1o1  29316  cusgrexg  29390  cusgrfilem3  29404  sizusglecusg  29410  wwlksnextbij  29851  gsumhashmul  33008  fzo0pmtrlast  33056  1arithidom  33505  gblacfnacd  35088  numiunnum  36446  bj-imdirco  37166  eqvreltr  38583  aks6d1c2  42106  sticksstones20  42142  onsucf1lem  43259  onsucf1olem  43260  nnoeomeqom  43302  rp-isfinite5  43507  clrellem  43612  clcnvlem  43613  fundcmpsurinj  47369  prproropen  47468  isuspgrim0  47845  grimidvtxedg  47849  grimcnv  47852  grimco  47853  gricushgr  47859  ushggricedg  47869  uhgrimisgrgric  47872  isgrtri  47883  usgrgrtrirex  47890  isubgr3stgrlem3  47908  isubgr3stgr  47915  uspgrlim  47932  grlimgrtri  47936  grlicref  47945  grlicsym  47946  grlictr  47948  uspgrsprfo  48037  uspgrbispr  48040  1aryenef  48539  2aryenef  48550  eufsnlem  48727  opncldeqv  48783  thincciso  49154  thinccisod  49155  functermceu  49208  idfudiag1  49223  termcarweu  49226  arweutermc  49228  mndtcbas  49273