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

Theorem rspcsbela 4215
Description: Special case related to rspsbc 3724. (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 3724 . . 3 (𝐴𝐵 → (∀𝑥𝐵 𝐶𝐷[𝐴 / 𝑥]𝐶𝐷))
2 sbcel1g 4195 . . 3 (𝐴𝐵 → ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐷))
31, 2sylibd 230 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝐶𝐷𝐴 / 𝑥𝐶𝐷))
43imp 395 1 ((𝐴𝐵 ∧ ∀𝑥𝐵 𝐶𝐷) → 𝐴 / 𝑥𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2157  wral 3107  [wsbc 3644  csb 3739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-nul 4128
This theorem is referenced by:  el2mpt2csbcl  7490  mptnn0fsupp  13027  mptnn0fsuppr  13029  fsumzcl2  14699  fsummsnunz  14713  fsumsplitsnun  14714  fsummsnunzOLD  14715  fsumsplitsnunOLD  14716  modfsummodslem1  14753  fprodmodd  14955  sumeven  15337  sumodd  15338  gsummpt1n0  18572  gsummptnn0fz  18590  gsummptnn0fzOLD  18591  telgsumfzslem  18594  telgsumfzs  18595  telgsums  18599  mptscmfsupp0  19139  coe1fzgsumdlem  19886  gsummoncoe1  19889  evl1gsumdlem  19935  madugsum  20668  iunmbl2  23548  gsumvsca1  30117  gsumvsca2  30118  esum2dlem  30489  esumiun  30491  iblsplitf  40670  fsummsndifre  41922  fsumsplitsndif  41923  fsummmodsndifre  41924  fsummmodsnunz  41925
  Copyright terms: Public domain W3C validator