Theorem rspcsbela 4443

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∀wral 3058  [wsbc 3790  ⦋csb 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-nul 4339

This theorem is referenced by:  el2mpocsbcl  8108  mptnn0fsupp  14034  mptnn0fsuppr  14036  fsumzcl2  15771  fsummsnunz  15786  fsumsplitsnun  15787  modfsummodslem1  15824  fprodmodd  16029  sumeven  16420  sumodd  16421  gsummpt1n0  19997  gsummptnn0fz  20018  telgsumfzslem  20020  telgsumfzs  20021  telgsums  20025  mptscmfsupp0  20941  coe1fzgsumdlem  22322  gsummoncoe1  22327  evl1gsumdlem  22375  madugsum  22664  iunmbl2  25605  gsumvsca1  33214  gsumvsca2  33215  rmfsupp2  33227  esum2dlem  34072  esumiun  34074  evl1gprodd  42098  idomnnzgmulnz  42114  deg1gprod  42121  f1o2d2  42252  iblsplitf  45925  fsummsndifre  47296  fsumsplitsndif  47297  fsummmodsndifre  47298  fsummmodsnunz  47299