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

Theorem rspcsbela 3958
 Description: Special case related to rspsbc 3484. (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 3484 . . 3 (𝐴𝐵 → (∀𝑥𝐵 𝐶𝐷[𝐴 / 𝑥]𝐶𝐷))
2 sbcel1g 3939 . . 3 (𝐴𝐵 → ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐷))
31, 2sylibd 228 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝐶𝐷𝐴 / 𝑥𝐶𝐷))
43imp 444 1 ((𝐴𝐵 ∧ ∀𝑥𝐵 𝐶𝐷) → 𝐴 / 𝑥𝐶𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896  [wsbc 3402  ⦋csb 3499 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-nul 3875 This theorem is referenced by:  el2mpt2csbcl  7137  mptnn0fsupp  12659  mptnn0fsuppr  12661  fsumzcl2  14316  fsummsnunz  14327  fsumsplitsnun  14328  modfsummodslem1  14365  fprodmodd  14567  sumeven  14948  sumodd  14949  gsummpt1n0  18187  gsummptnn0fz  18205  telgsumfzslem  18208  telgsumfzs  18209  telgsums  18213  mptscmfsupp0  18751  coe1fzgsumdlem  19492  gsummoncoe1  19495  evl1gsumdlem  19541  madugsum  20268  iunmbl2  23132  gsumvsca1  29113  gsumvsca2  29114  esum2dlem  29481  esumiun  29483  iblsplitf  38862  fsummsndifre  40371  fsumsplitsndif  40372  fsummmodsndifre  40373  fsummmodsnunz  40374
 Copyright terms: Public domain W3C validator