Theorem rspcsbela 4461

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3067  [wsbc 3804  ⦋csb 3921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-nul 4353

This theorem is referenced by:  el2mpocsbcl  8126  mptnn0fsupp  14048  mptnn0fsuppr  14050  fsumzcl2  15787  fsummsnunz  15802  fsumsplitsnun  15803  modfsummodslem1  15840  fprodmodd  16045  sumeven  16435  sumodd  16436  gsummpt1n0  20007  gsummptnn0fz  20028  telgsumfzslem  20030  telgsumfzs  20031  telgsums  20035  mptscmfsupp0  20947  coe1fzgsumdlem  22328  gsummoncoe1  22333  evl1gsumdlem  22381  madugsum  22670  iunmbl2  25611  gsumvsca1  33205  gsumvsca2  33206  rmfsupp2  33218  esum2dlem  34056  esumiun  34058  evl1gprodd  42074  idomnnzgmulnz  42090  deg1gprod  42097  f1o2d2  42228  iblsplitf  45891  fsummsndifre  47246  fsumsplitsndif  47247  fsummmodsndifre  47248  fsummmodsnunz  47249