Theorem rspcsbela 4386

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110  ∀wral 3138  [wsbc 3771  ⦋csb 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-nul 4291

This theorem is referenced by:  el2mpocsbcl  7779  mptnn0fsupp  13364  mptnn0fsuppr  13366  fsumzcl2  15094  fsummsnunz  15108  fsumsplitsnun  15109  modfsummodslem1  15146  fprodmodd  15350  sumeven  15737  sumodd  15738  gsummpt1n0  19084  gsummptnn0fz  19105  telgsumfzslem  19107  telgsumfzs  19108  telgsums  19112  mptscmfsupp0  19698  coe1fzgsumdlem  20468  gsummoncoe1  20471  evl1gsumdlem  20518  madugsum  21251  iunmbl2  24157  gsumvsca1  30854  gsumvsca2  30855  rmfsupp2  30866  esum2dlem  31351  esumiun  31353  iblsplitf  42253  fsummsndifre  43531  fsumsplitsndif  43532  fsummmodsndifre  43533  fsummmodsnunz  43534