Theorem rspcsbela 4389

Description: Special case related to rspsbc 3830. (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 3830	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → [𝐴 / 𝑥]𝐶 ∈ 𝐷))
2		sbcel1g 4367	. . 3 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ∈ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷))
3	1, 2	sylibd 241	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷))
4	3	imp 410	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∀wral 3075  [wsbc 3742  ⦋csb 3850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-nul 4284

This theorem is referenced by:  el2mpocsbcl  8058  mpof1o2d  8099  mptnn0fsupp  14004  mptnn0fsuppr  14006  fsumzcl2  15757  fsummsnunz  15772  fsumsplitsnun  15773  modfsummodslem1  15811  fprodmodd  16018  sumeven  16412  sumodd  16413  gsummpt1n0  19996  gsummptnn0fz  20017  telgsumfzslem  20019  telgsumfzs  20020  telgsums  20024  mptscmfsupp0  20982  coe1fzgsumdlem  22354  gsummoncoe1  22359  evl1gsumdlem  22407  madugsum  22691  iunmbl2  25607  gsummptfzsplitra  33199  gsummptfzsplitla  33200  gsummulsubdishift1s  33211  gsummulsubdishift2s  33212  gsumvsca1  33367  gsumvsca2  33368  rmfsupp2  33379  esum2dlem  34350  esumiun  34352  evl1gprodd  42695  idomnnzgmulnz  42711  deg1gprod  42718  iblsplitf  46505  fsummsndifre  47935  fsumsplitsndif  47936  fsummmodsndifre  47937  fsummmodsnunz  47938