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 3861. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
Ref | Expression |
---|---|
rspcsbela | ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspsbc 3861 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → [𝐴 / 𝑥]𝐶 ∈ 𝐷)) | |
2 | sbcel1g 4364 | . . 3 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ∈ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)) | |
3 | 1, 2 | sylibd 241 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)) |
4 | 3 | imp 409 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∈ wcel 2110 ∀wral 3138 [wsbc 3771 ⦋csb 3882 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-nul 4291 |
This theorem is referenced by: el2mpocsbcl 7774 mptnn0fsupp 13359 mptnn0fsuppr 13361 fsumzcl2 15089 fsummsnunz 15103 fsumsplitsnun 15104 modfsummodslem1 15141 fprodmodd 15345 sumeven 15732 sumodd 15733 gsummpt1n0 19079 gsummptnn0fz 19100 telgsumfzslem 19102 telgsumfzs 19103 telgsums 19107 mptscmfsupp0 19693 coe1fzgsumdlem 20463 gsummoncoe1 20466 evl1gsumdlem 20513 madugsum 21246 iunmbl2 24152 gsumvsca1 30849 gsumvsca2 30850 rmfsupp2 30861 esum2dlem 31346 esumiun 31348 iblsplitf 42248 fsummsndifre 43526 fsumsplitsndif 43527 fsummmodsndifre 43528 fsummmodsnunz 43529 |
Copyright terms: Public domain | W3C validator |