Theorem rspcsbela 4379

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2105  ∀wral 3061  [wsbc 3725  ⦋csb 3841

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-nul 4267

This theorem is referenced by:  el2mpocsbcl  7971  mptnn0fsupp  13796  mptnn0fsuppr  13798  fsumzcl2  15527  fsummsnunz  15542  fsumsplitsnun  15543  modfsummodslem1  15580  fprodmodd  15783  sumeven  16172  sumodd  16173  gsummpt1n0  19638  gsummptnn0fz  19659  telgsumfzslem  19661  telgsumfzs  19662  telgsums  19666  mptscmfsupp0  20268  coe1fzgsumdlem  21552  gsummoncoe1  21555  evl1gsumdlem  21602  madugsum  21872  iunmbl2  24801  gsumvsca1  31610  gsumvsca2  31611  rmfsupp2  31623  esum2dlem  32196  esumiun  32198  iblsplitf  43766  fsummsndifre  45094  fsumsplitsndif  45095  fsummmodsndifre  45096  fsummmodsnunz  45097