Theorem rspcsbela 4396

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3077  [wsbc 3739  ⦋csb 3847

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-nul 4280

This theorem is used by:  el2mpocsbcl  8094  mpof1o2d  8135  mptnn0fsupp  14133  mptnn0fsuppr  14135  fsumzcl2  15898  fsummsnunz  15913  fsumsplitsnun  15914  modfsummodslem1  15952  fprodmodd  16157  sumeven  16550  sumodd  16551  gsummpt1n0  20172  gsummptnn0fz  20193  telgsumfzslem  20195  telgsumfzs  20196  telgsums  20200  mptscmfsupp0  21195  coe1fzgsumdlem  22614  gsummoncoe1  22619  evl1gsumdlem  22667  madugsum  22951  iunmbl2  25871  gsummptfzsplitra  33612  gsummptfzsplitla  33613  gsummulsubdishift1s  33624  gsummulsubdishift2s  33625  gsumvsca1  33780  gsumvsca2  33781  rmfsupp2  33791  esum2dlem  34717  esumiun  34719  evl1gprodd  43147  idomnnzgmulnz  43163  deg1gprod  43170  iblsplitf  46949  fsummsndifre  48419  fsumsplitsndif  48420  fsummmodsndifre  48421  fsummmodsnunz  48422