Theorem rspcsbela 4266

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

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2051  ∀wral 3083  [wsbc 3676  ⦋csb 3781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-fal 1521  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ral 3088  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-nul 4174

This theorem is referenced by:  el2mpocsbcl  7587  mptnn0fsupp  13179  mptnn0fsuppr  13181  fsumzcl2  14954  fsummsnunz  14968  fsumsplitsnun  14969  modfsummodslem1  15006  fprodmodd  15210  sumeven  15597  sumodd  15598  gsummpt1n0  18851  gsummptnn0fz  18869  telgsumfzslem  18871  telgsumfzs  18872  telgsums  18876  mptscmfsupp0  19434  coe1fzgsumdlem  20188  gsummoncoe1  20191  evl1gsumdlem  20237  madugsum  20972  iunmbl2  23877  gsumvsca1  30558  gsumvsca2  30559  rmfsupp2  30578  esum2dlem  31028  esumiun  31030  iblsplitf  41715  fsummsndifre  42968  fsumsplitsndif  42969  fsummmodsndifre  42970  fsummmodsnunz  42971