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  43883  onsucf1olem  43884  nnoeomeqom  43926  rp-isfinite5  44130  clrellem  44235  clcnvlem  44236  fundcmpsurinj  48042  prproropen  48141  grimidvtxedg  48534  grimcnv  48537  grimco  48538  isuspgrim0  48543  gricushgr  48566  ushggricedg  48576  uhgrimisgrgric  48580  isgrtri  48592  usgrgrtrirex  48599  isubgr3stgrlem3  48617  isubgr3stgr  48624  uspgrlim  48641  grlimgrtri  48652  grlicref  48661  grlicsym  48662  grlictr  48664  uspgrsprfo  48797  uspgrbispr  48800  1aryenef  49305  2aryenef  49316  eufsnlem  49499  xpco2  49515  opncldeqv  49560  uobffth  49876  uobeqw  49877  thincciso  50111  thinccisod  50112  functermceu  50168  idfudiag1  50183  termcarweu  50186  arweutermc  50188  funcsn  50199  0fucterm  50201  mndtcbas  50239