Theorem rspcsbela 4390

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3051  [wsbc 3740  ⦋csb 3849

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 2184  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-nul 4286

This theorem is referenced by:  el2mpocsbcl  8027  mptnn0fsupp  13920  mptnn0fsuppr  13922  fsumzcl2  15662  fsummsnunz  15677  fsumsplitsnun  15678  modfsummodslem1  15715  fprodmodd  15920  sumeven  16314  sumodd  16315  gsummpt1n0  19894  gsummptnn0fz  19915  telgsumfzslem  19917  telgsumfzs  19918  telgsums  19922  mptscmfsupp0  20878  coe1fzgsumdlem  22247  gsummoncoe1  22252  evl1gsumdlem  22300  madugsum  22587  iunmbl2  25514  gsummptfzsplitra  33141  gsummptfzsplitla  33142  gsummulsubdishift1s  33153  gsummulsubdishift2s  33154  gsumvsca1  33308  gsumvsca2  33309  rmfsupp2  33320  esum2dlem  34249  esumiun  34251  evl1gprodd  42371  idomnnzgmulnz  42387  deg1gprod  42394  f1o2d2  42489  iblsplitf  46214  fsummsndifre  47618  fsumsplitsndif  47619  fsummmodsndifre  47620  fsummmodsnunz  47621