Theorem rspcsbela 4387

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3048  [wsbc 3737  ⦋csb 3846

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 2182  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-nul 4283

This theorem is referenced by:  el2mpocsbcl  8021  mptnn0fsupp  13906  mptnn0fsuppr  13908  fsumzcl2  15648  fsummsnunz  15663  fsumsplitsnun  15664  modfsummodslem1  15701  fprodmodd  15906  sumeven  16300  sumodd  16301  gsummpt1n0  19879  gsummptnn0fz  19900  telgsumfzslem  19902  telgsumfzs  19903  telgsums  19907  mptscmfsupp0  20862  coe1fzgsumdlem  22219  gsummoncoe1  22224  evl1gsumdlem  22272  madugsum  22559  iunmbl2  25486  gsumvsca1  33202  gsumvsca2  33203  rmfsupp2  33212  esum2dlem  34126  esumiun  34128  evl1gprodd  42230  idomnnzgmulnz  42246  deg1gprod  42253  f1o2d2  42351  iblsplitf  46092  fsummsndifre  47496  fsumsplitsndif  47497  fsummmodsndifre  47498  fsummmodsnunz  47499