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 3900  df-nul 4280

This theorem is used by:  el2mpocsbcl  8097  mpof1o2d  8138  mptnn0fsupp  14141  mptnn0fsuppr  14143  fsumzcl2  15906  fsummsnunz  15921  fsumsplitsnun  15922  modfsummodslem1  15960  fprodmodd  16165  sumeven  16558  sumodd  16559  gsummpt1n0  20180  gsummptnn0fz  20201  telgsumfzslem  20203  telgsumfzs  20204  telgsums  20208  mptscmfsupp0  21203  coe1fzgsumdlem  22622  gsummoncoe1  22627  evl1gsumdlem  22675  madugsum  22959  iunmbl2  25879  gsummptfzsplitra  33620  gsummptfzsplitla  33621  gsummulsubdishift1s  33632  gsummulsubdishift2s  33633  gsumvsca1  33788  gsumvsca2  33789  rmfsupp2  33799  esum2dlem  34725  esumiun  34727  evl1gprodd  43169  idomnnzgmulnz  43185  deg1gprod  43192  iblsplitf  46981  fsummsndifre  48451  fsumsplitsndif  48452  fsummmodsndifre  48453  fsummmodsnunz  48454