Theorem rspcsbela 4366

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∀wral 3053  [wsbc 3723  ⦋csb 3831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-nul 4262

This theorem is referenced by:  el2mpocsbcl  8024  mpof1o2d  8065  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  20917  coe1fzgsumdlem  22289  gsummoncoe1  22294  evl1gsumdlem  22342  madugsum  22626  iunmbl2  25542  gsummptfzsplitra  33139  gsummptfzsplitla  33140  gsummulsubdishift1s  33151  gsummulsubdishift2s  33152  gsumvsca1  33307  gsumvsca2  33308  rmfsupp2  33319  esum2dlem  34276  esumiun  34278  evl1gprodd  42602  idomnnzgmulnz  42618  deg1gprod  42625  iblsplitf  46413  fsummsndifre  47843  fsumsplitsndif  47844  fsummmodsndifre  47845  fsummmodsnunz  47846