Theorem rspcsbela 4340

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110  ∀wral 3054  [wsbc 3687  ⦋csb 3802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ral 3059  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-nul 4228

This theorem is referenced by:  el2mpocsbcl  7842  mptnn0fsupp  13553  mptnn0fsuppr  13555  fsumzcl2  15285  fsummsnunz  15299  fsumsplitsnun  15300  modfsummodslem1  15337  fprodmodd  15540  sumeven  15929  sumodd  15930  gsummpt1n0  19322  gsummptnn0fz  19343  telgsumfzslem  19345  telgsumfzs  19346  telgsums  19350  mptscmfsupp0  19936  coe1fzgsumdlem  21194  gsummoncoe1  21197  evl1gsumdlem  21244  madugsum  21512  iunmbl2  24426  gsumvsca1  31170  gsumvsca2  31171  rmfsupp2  31183  esum2dlem  31744  esumiun  31746  iblsplitf  43140  fsummsndifre  44451  fsumsplitsndif  44452  fsummmodsndifre  44453  fsummmodsnunz  44454