Theorem rspcsbela 4387

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3048  [wsbc 3737  ⦋csb 3846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-nul 4283

This theorem is referenced by:  el2mpocsbcl  8024  mptnn0fsupp  13911  mptnn0fsuppr  13913  fsumzcl2  15653  fsummsnunz  15668  fsumsplitsnun  15669  modfsummodslem1  15706  fprodmodd  15911  sumeven  16305  sumodd  16306  gsummpt1n0  19885  gsummptnn0fz  19906  telgsumfzslem  19908  telgsumfzs  19909  telgsums  19913  mptscmfsupp0  20869  coe1fzgsumdlem  22238  gsummoncoe1  22243  evl1gsumdlem  22291  madugsum  22578  iunmbl2  25505  gsummptfzsplitra  33069  gsummptfzsplitla  33070  gsummulsubdishift1s  33081  gsummulsubdishift2s  33082  gsumvsca1  33236  gsumvsca2  33237  rmfsupp2  33248  esum2dlem  34177  esumiun  34179  evl1gprodd  42283  idomnnzgmulnz  42299  deg1gprod  42306  f1o2d2  42404  iblsplitf  46130  fsummsndifre  47534  fsumsplitsndif  47535  fsummmodsndifre  47536  fsummmodsnunz  47537