MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  spcedv Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 spcedv.1 . 2 (𝜑𝑋𝑉)
2 spcedv.2 . 2 (𝜑𝜒)
3 spcedv.3 . . 3 (𝑥 = 𝑋 → (𝜓𝜒))
43spcegv 3597 . 2 (𝑋𝑉 → (𝜒 → ∃𝑥𝜓))
51, 2, 4sylc 65 1 (𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator