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

Theorem rspcsbela 3953
Description: Special case related to rspsbc 3479. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)
Assertion
Ref Expression
rspcsbela ((𝐴𝐵 ∧ ∀𝑥𝐵 𝐶𝐷) → 𝐴 / 𝑥𝐶𝐷)
Distinct variable groups:   𝑥,𝐵   𝑥,𝐷
Allowed substitution hints:   𝐴(𝑥)   𝐶(𝑥)

Proof of Theorem rspcsbela
StepHypRef Expression
1 rspsbc 3479 . . 3 (𝐴𝐵 → (∀𝑥𝐵 𝐶𝐷[𝐴 / 𝑥]𝐶𝐷))
2 sbcel1g 3934 . . 3 (𝐴𝐵 → ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐷))
31, 2sylibd 227 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝐶𝐷𝐴 / 𝑥𝐶𝐷))
43imp 443 1 ((𝐴𝐵 ∧ ∀𝑥𝐵 𝐶𝐷) → 𝐴 / 𝑥𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1975  wral 2891  [wsbc 3397  csb 3494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-nul 3870
This theorem is referenced by:  el2mpt2csbcl  7110  mptnn0fsupp  12610  mptnn0fsuppr  12612  fsumzcl2  14258  fsummsnunz  14269  fsumsplitsnun  14270  modfsummodslem1  14307  fprodmodd  14509  sumeven  14890  sumodd  14891  gsummpt1n0  18129  gsummptnn0fz  18147  telgsumfzslem  18150  telgsumfzs  18151  telgsums  18155  mptscmfsupp0  18693  coe1fzgsumdlem  19434  gsummoncoe1  19437  evl1gsumdlem  19483  madugsum  20206  iunmbl2  23045  gsumvsca1  28915  gsumvsca2  28916  esum2dlem  29283  esumiun  29285  iblsplitf  38662  fsummsndifre  40217  fsumsplitsndif  40218  fsummmodsndifre  40219  fsummmodsnunz  40220
  Copyright terms: Public domain W3C validator