Theorem rspcsbela 4392

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052  [wsbc 3742  ⦋csb 3851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-nul 4288

This theorem is referenced by:  el2mpocsbcl  8037  mptnn0fsupp  13932  mptnn0fsuppr  13934  fsumzcl2  15674  fsummsnunz  15689  fsumsplitsnun  15690  modfsummodslem1  15727  fprodmodd  15932  sumeven  16326  sumodd  16327  gsummpt1n0  19906  gsummptnn0fz  19927  telgsumfzslem  19929  telgsumfzs  19930  telgsums  19934  mptscmfsupp0  20890  coe1fzgsumdlem  22259  gsummoncoe1  22264  evl1gsumdlem  22312  madugsum  22599  iunmbl2  25526  gsummptfzsplitra  33152  gsummptfzsplitla  33153  gsummulsubdishift1s  33164  gsummulsubdishift2s  33165  gsumvsca1  33320  gsumvsca2  33321  rmfsupp2  33332  esum2dlem  34270  esumiun  34272  evl1gprodd  42487  idomnnzgmulnz  42503  deg1gprod  42510  f1o2d2  42605  iblsplitf  46328  fsummsndifre  47732  fsumsplitsndif  47733  fsummmodsndifre  47734  fsummmodsnunz  47735