Theorem rspcsbela 4404

Description: Special case related to rspsbc 3845. (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

Step	Hyp	Ref	Expression
1		rspsbc 3845	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → [𝐴 / 𝑥]𝐶 ∈ 𝐷))
2		sbcel1g 4382	. . 3 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ∈ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷))
3	1, 2	sylibd 239	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷))
4	3	imp 406	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3045  [wsbc 3756  ⦋csb 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-nul 4300

This theorem is referenced by:  el2mpocsbcl  8067  mptnn0fsupp  13969  mptnn0fsuppr  13971  fsumzcl2  15712  fsummsnunz  15727  fsumsplitsnun  15728  modfsummodslem1  15765  fprodmodd  15970  sumeven  16364  sumodd  16365  gsummpt1n0  19902  gsummptnn0fz  19923  telgsumfzslem  19925  telgsumfzs  19926  telgsums  19930  mptscmfsupp0  20840  coe1fzgsumdlem  22197  gsummoncoe1  22202  evl1gsumdlem  22250  madugsum  22537  iunmbl2  25465  gsumvsca1  33186  gsumvsca2  33187  rmfsupp2  33196  esum2dlem  34089  esumiun  34091  evl1gprodd  42112  idomnnzgmulnz  42128  deg1gprod  42135  f1o2d2  42228  iblsplitf  45975  fsummsndifre  47377  fsumsplitsndif  47378  fsummmodsndifre  47379  fsummmodsnunz  47380