Theorem rspcsbela 4378

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3051  [wsbc 3728  ⦋csb 3837

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-nul 4274

This theorem is referenced by:  el2mpocsbcl  8035  mptnn0fsupp  13959  mptnn0fsuppr  13961  fsumzcl2  15701  fsummsnunz  15716  fsumsplitsnun  15717  modfsummodslem1  15755  fprodmodd  15962  sumeven  16356  sumodd  16357  gsummpt1n0  19940  gsummptnn0fz  19961  telgsumfzslem  19963  telgsumfzs  19964  telgsums  19968  mptscmfsupp0  20922  coe1fzgsumdlem  22268  gsummoncoe1  22273  evl1gsumdlem  22321  madugsum  22608  iunmbl2  25524  gsummptfzsplitra  33119  gsummptfzsplitla  33120  gsummulsubdishift1s  33131  gsummulsubdishift2s  33132  gsumvsca1  33287  gsumvsca2  33288  rmfsupp2  33299  esum2dlem  34236  esumiun  34238  evl1gprodd  42556  idomnnzgmulnz  42572  deg1gprod  42579  f1o2d2  42674  iblsplitf  46398  fsummsndifre  47828  fsumsplitsndif  47829  fsummmodsndifre  47830  fsummmodsnunz  47831