Theorem rspcsbela 4379

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

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

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 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-nul 4275

This theorem is referenced by:  el2mpocsbcl  8028  mptnn0fsupp  13950  mptnn0fsuppr  13952  fsumzcl2  15692  fsummsnunz  15707  fsumsplitsnun  15708  modfsummodslem1  15746  fprodmodd  15953  sumeven  16347  sumodd  16348  gsummpt1n0  19931  gsummptnn0fz  19952  telgsumfzslem  19954  telgsumfzs  19955  telgsums  19959  mptscmfsupp0  20913  coe1fzgsumdlem  22278  gsummoncoe1  22283  evl1gsumdlem  22331  madugsum  22618  iunmbl2  25534  gsummptfzsplitra  33134  gsummptfzsplitla  33135  gsummulsubdishift1s  33146  gsummulsubdishift2s  33147  gsumvsca1  33302  gsumvsca2  33303  rmfsupp2  33314  esum2dlem  34252  esumiun  34254  evl1gprodd  42570  idomnnzgmulnz  42586  deg1gprod  42593  f1o2d2  42688  iblsplitf  46416  fsummsndifre  47840  fsumsplitsndif  47841  fsummmodsndifre  47842  fsummmodsnunz  47843