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

Theorem spcedv 3546
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 3545 . 2 (𝑋𝑉 → (𝜒 → ∃𝑥𝜓))
51, 2, 4sylc 65 1 (𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1540  wex 1780  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-clel 2814
This theorem is referenced by:  selsALT  5384  zfrep6  7865  wfrlem15OLD  8224  ertr  8584  f1dom2gOLD  8831  dom3d  8855  disjenex  9000  domssex2  9002  domssex  9003  brwdom2  9430  infxpenc2lem2  9877  dfac8clem  9889  ac5num  9893  acni2  9903  acnlem  9905  finnisoeu  9970  infpss  10074  cofsmo  10126  axdc4lem  10312  ac6num  10336  axdclem2  10377  hasheqf1od  14168  fz1isolem  14275  wrd2f1tovbij  14774  fsum  15531  ntrivcvgn0  15709  fprod  15750  setsexstruct2  16973  isacs1i  17463  mreacs  17464  gsumval3lem2  19602  eltg3  22218  elptr  22830  nbusgrf1o1  28026  cusgrexg  28100  cusgrfilem3  28113  sizusglecusg  28119  wwlksnextbij  28555  gsumhashmul  31603  bj-imdirco  35474  eqvreltr  36882  sticksstones20  40387  rp-isfinite5  41454  clrellem  41559  clcnvlem  41560  fundcmpsurinj  45220  prproropen  45319  isomgreqve  45636  isomushgr  45637  isomgrsym  45647  isomgrtr  45650  ushrisomgr  45652  uspgrsprfo  45669  uspgrbispr  45672  1aryenef  46350  2aryenef  46361  eufsnlem  46527  opncldeqv  46554  thincciso  46689  mndtcbas  46727
  Copyright terms: Public domain W3C validator