Theorem rspcsbela 4403

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 4381	. . 3 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ∈ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷))
3	1, 2	sylibd 242	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷))
4	3	imp 412	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ∀wral 3081  [wsbc 3746  ⦋csb 3854

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-nul 4287

This theorem is used by:  el2mpocsbcl  8086  mpof1o2d  8127  mptnn0fsupp  14051  mptnn0fsuppr  14053  fsumzcl2  15813  fsummsnunz  15828  fsumsplitsnun  15829  modfsummodslem1  15867  fprodmodd  16074  sumeven  16467  sumodd  16468  gsummpt1n0  20079  gsummptnn0fz  20100  telgsumfzslem  20102  telgsumfzs  20103  telgsums  20107  mptscmfsupp0  21098  coe1fzgsumdlem  22513  gsummoncoe1  22518  evl1gsumdlem  22566  madugsum  22850  iunmbl2  25767  gsummptfzsplitra  33442  gsummptfzsplitla  33443  gsummulsubdishift1s  33454  gsummulsubdishift2s  33455  gsumvsca1  33610  gsumvsca2  33611  rmfsupp2  33621  esum2dlem  34546  esumiun  34548  evl1gprodd  42942  idomnnzgmulnz  42958  deg1gprod  42965  iblsplitf  46742  fsummsndifre  48175  fsumsplitsndif  48176  fsummmodsndifre  48177  fsummmodsnunz  48178