Theorem spcedv 3566

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ∃wex 1806   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-clel 2844

This theorem is referenced by:  selsALT  5420  zfrep6OLD  7948  ertr  8706  dom3d  8987  disjenex  9119  domssex2  9121  domssex  9122  brwdom2  9531  infxpenc2lem2  10000  dfac8clem  10012  ac5num  10016  acni2  10026  acnlem  10028  finnisoeu  10093  infpss  10195  cofsmo  10249  axdc4lem  10435  ac6num  10459  axdclem2  10500  hasheqf1od  14385  fz1isolem  14494  wrd2f1tovbij  14993  fsum  15767  ntrivcvgn0  15948  fprod  15991  setsexstruct2  17231  isacs1i  17709  mreacs  17710  gsumval3lem2  19972  eltg3  23084  elptr  23695  oldfib  28532  nbusgrf1o1  29657  cusgrexg  29731  cusgrfilem3  29744  sizusglecusg  29750  wwlksnextbij  30188  gsumhashmul  33324  fzo0pmtrlast  33349  1arithidom  33768  fineqvnttrclse  35456  gblacfnacd  35481  onvfowev  35495  numiunnum  36866  bj-imdirco  37717  eqvreltr  39225  aks6d1c2  42782  sticksstones20  42818  onsucf1lem  43881  onsucf1olem  43882  nnoeomeqom  43924  rp-isfinite5  44128  clrellem  44233  clcnvlem  44234  fundcmpsurinj  48040  prproropen  48139  grimidvtxedg  48532  grimcnv  48535  grimco  48536  isuspgrim0  48541  gricushgr  48564  ushggricedg  48574  uhgrimisgrgric  48578  isgrtri  48590  usgrgrtrirex  48597  isubgr3stgrlem3  48615  isubgr3stgr  48622  uspgrlim  48639  grlimgrtri  48650  grlicref  48659  grlicsym  48660  grlictr  48662  uspgrsprfo  48795  uspgrbispr  48798  1aryenef  49303  2aryenef  49314  eufsnlem  49497  xpco2  49513  opncldeqv  49558  uobffth  49874  uobeqw  49875  thincciso  50109  thinccisod  50110  functermceu  50166  idfudiag1  50181  termcarweu  50184  arweutermc  50186  funcsn  50197  0fucterm  50199  mndtcbas  50237