Theorem rspcsbela 4403

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∀wral 3079  [wsbc 3744  ⦋csb 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-nul 4287

This theorem is referenced by:  el2mpocsbcl  8076  mpof1o2d  8117  mptnn0fsupp  14029  mptnn0fsuppr  14031  fsumzcl2  15786  fsummsnunz  15801  fsumsplitsnun  15802  modfsummodslem1  15840  fprodmodd  16047  sumeven  16440  sumodd  16441  gsummpt1n0  20030  gsummptnn0fz  20051  telgsumfzslem  20053  telgsumfzs  20054  telgsums  20058  mptscmfsupp0  21048  coe1fzgsumdlem  22463  gsummoncoe1  22468  evl1gsumdlem  22516  madugsum  22800  iunmbl2  25716  gsummptfzsplitra  33378  gsummptfzsplitla  33379  gsummulsubdishift1s  33390  gsummulsubdishift2s  33391  gsumvsca1  33546  gsumvsca2  33547  rmfsupp2  33557  esum2dlem  34482  esumiun  34484  evl1gprodd  42884  idomnnzgmulnz  42900  deg1gprod  42907  iblsplitf  46684  fsummsndifre  48117  fsumsplitsndif  48118  fsummmodsndifre  48119  fsummmodsnunz  48120