Theorem rspcsbela 4039

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2030  ∀wral 2941  [wsbc 3468  ⦋csb 3566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-nul 3949

This theorem is referenced by:  el2mpt2csbcl  7295  mptnn0fsupp  12837  mptnn0fsuppr  12839  fsumzcl2  14513  fsummsnunz  14527  fsumsplitsnun  14528  fsummsnunzOLD  14529  fsumsplitsnunOLD  14530  modfsummodslem1  14568  fprodmodd  14772  sumeven  15157  sumodd  15158  gsummpt1n0  18410  gsummptnn0fz  18428  telgsumfzslem  18431  telgsumfzs  18432  telgsums  18436  mptscmfsupp0  18976  coe1fzgsumdlem  19719  gsummoncoe1  19722  evl1gsumdlem  19768  madugsum  20497  iunmbl2  23371  gsumvsca1  29910  gsumvsca2  29911  esum2dlem  30282  esumiun  30284  iblsplitf  40504  fsummsndifre  41667  fsumsplitsndif  41668  fsummmodsndifre  41669  fsummmodsnunz  41670