![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspcsbela | Structured version Visualization version GIF version |
Description: Special case related to rspsbc 3874. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
Ref | Expression |
---|---|
rspcsbela | ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspsbc 3874 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → [𝐴 / 𝑥]𝐶 ∈ 𝐷)) | |
2 | sbcel1g 4414 | . . 3 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ∈ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)) | |
3 | 1, 2 | sylibd 238 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)) |
4 | 3 | imp 408 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ∀wral 3062 [wsbc 3778 ⦋csb 3894 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-nul 4324 |
This theorem is referenced by: el2mpocsbcl 8071 mptnn0fsupp 13962 mptnn0fsuppr 13964 fsumzcl2 15685 fsummsnunz 15700 fsumsplitsnun 15701 modfsummodslem1 15738 fprodmodd 15941 sumeven 16330 sumodd 16331 gsummpt1n0 19833 gsummptnn0fz 19854 telgsumfzslem 19856 telgsumfzs 19857 telgsums 19861 mptscmfsupp0 20537 coe1fzgsumdlem 21825 gsummoncoe1 21828 evl1gsumdlem 21875 madugsum 22145 iunmbl2 25074 gsumvsca1 32371 gsumvsca2 32372 rmfsupp2 32387 esum2dlem 33090 esumiun 33092 f1o2d2 41055 iblsplitf 44686 fsummsndifre 46040 fsumsplitsndif 46041 fsummmodsndifre 46042 fsummmodsnunz 46043 |
Copyright terms: Public domain | W3C validator |