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

Theorem rspcsbela 4039
Description: Special case related to rspsbc 3551. (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 3551 . . 3 (𝐴𝐵 → (∀𝑥𝐵 𝐶𝐷[𝐴 / 𝑥]𝐶𝐷))
2 sbcel1g 4020 . . 3 (𝐴𝐵 → ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐷))
31, 2sylibd 229 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝐶𝐷𝐴 / 𝑥𝐶𝐷))
43imp 444 1 ((𝐴𝐵 ∧ ∀𝑥𝐵 𝐶𝐷) → 𝐴 / 𝑥𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wral 2941  [wsbc 3468  csb 3566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-nul 3949
This theorem is referenced by:  el2mpt2csbcl  7295  mptnn0fsupp  12837  mptnn0fsuppr  12839  fsumzcl2  14513  fsummsnunz  14527  fsumsplitsnun  14528  fsummsnunzOLD  14529  fsumsplitsnunOLD  14530  modfsummodslem1  14568  fprodmodd  14772  sumeven  15157  sumodd  15158  gsummpt1n0  18410  gsummptnn0fz  18428  telgsumfzslem  18431  telgsumfzs  18432  telgsums  18436  mptscmfsupp0  18976  coe1fzgsumdlem  19719  gsummoncoe1  19722  evl1gsumdlem  19768  madugsum  20497  iunmbl2  23371  gsumvsca1  29910  gsumvsca2  29911  esum2dlem  30282  esumiun  30284  iblsplitf  40504  fsummsndifre  41667  fsumsplitsndif  41668  fsummmodsndifre  41669  fsummmodsnunz  41670
  Copyright terms: Public domain W3C validator