Theorem rspcsbela 4401

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∀wral 3085  [wsbc 3753  ⦋csb 3861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-nul 4295

This theorem is referenced by:  el2mpocsbcl  8076  mpof1o2d  8117  mptnn0fsupp  14029  mptnn0fsuppr  14031  fsumzcl2  15786  fsummsnunz  15801  fsumsplitsnun  15802  modfsummodslem1  15840  fprodmodd  16047  sumeven  16441  sumodd  16442  gsummpt1n0  20031  gsummptnn0fz  20052  telgsumfzslem  20054  telgsumfzs  20055  telgsums  20059  mptscmfsupp0  21022  coe1fzgsumdlem  22428  gsummoncoe1  22433  evl1gsumdlem  22481  madugsum  22765  iunmbl2  25681  gsummptfzsplitra  33315  gsummptfzsplitla  33316  gsummulsubdishift1s  33327  gsummulsubdishift2s  33328  gsumvsca1  33483  gsumvsca2  33484  rmfsupp2  33494  esum2dlem  34423  esumiun  34425  evl1gprodd  42769  idomnnzgmulnz  42785  deg1gprod  42792  iblsplitf  46571  fsummsndifre  48001  fsumsplitsndif  48002  fsummmodsndifre  48003  fsummmodsnunz  48004