Theorem rspcsbela 3958

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896  [wsbc 3402  ⦋csb 3499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-nul 3875

This theorem is referenced by:  el2mpt2csbcl  7137  mptnn0fsupp  12659  mptnn0fsuppr  12661  fsumzcl2  14316  fsummsnunz  14327  fsumsplitsnun  14328  modfsummodslem1  14365  fprodmodd  14567  sumeven  14948  sumodd  14949  gsummpt1n0  18187  gsummptnn0fz  18205  telgsumfzslem  18208  telgsumfzs  18209  telgsums  18213  mptscmfsupp0  18751  coe1fzgsumdlem  19492  gsummoncoe1  19495  evl1gsumdlem  19541  madugsum  20268  iunmbl2  23132  gsumvsca1  29113  gsumvsca2  29114  esum2dlem  29481  esumiun  29483  iblsplitf  38862  fsummsndifre  40371  fsumsplitsndif  40372  fsummmodsndifre  40373  fsummmodsnunz  40374