Theorem rspcsbela 4391

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044  [wsbc 3744  ⦋csb 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-nul 4287

This theorem is referenced by:  el2mpocsbcl  8025  mptnn0fsupp  13923  mptnn0fsuppr  13925  fsumzcl2  15665  fsummsnunz  15680  fsumsplitsnun  15681  modfsummodslem1  15718  fprodmodd  15923  sumeven  16317  sumodd  16318  gsummpt1n0  19863  gsummptnn0fz  19884  telgsumfzslem  19886  telgsumfzs  19887  telgsums  19891  mptscmfsupp0  20849  coe1fzgsumdlem  22207  gsummoncoe1  22212  evl1gsumdlem  22260  madugsum  22547  iunmbl2  25475  gsumvsca1  33187  gsumvsca2  33188  rmfsupp2  33197  esum2dlem  34078  esumiun  34080  evl1gprodd  42110  idomnnzgmulnz  42126  deg1gprod  42133  f1o2d2  42226  iblsplitf  45971  fsummsndifre  47376  fsumsplitsndif  47377  fsummmodsndifre  47378  fsummmodsnunz  47379