![]() |
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 3873. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.) |
Ref | Expression |
---|---|
rspcsbela | ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspsbc 3873 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → [𝐴 / 𝑥]𝐶 ∈ 𝐷)) | |
2 | sbcel1g 4413 | . . 3 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 ∈ 𝐷 ↔ ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)) | |
3 | 1, 2 | sylibd 238 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷)) |
4 | 3 | imp 407 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝐶 ∈ 𝐷) → ⦋𝐴 / 𝑥⦌𝐶 ∈ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2106 ∀wral 3061 [wsbc 3777 ⦋csb 3893 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ral 3062 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-nul 4323 |
This theorem is referenced by: el2mpocsbcl 8073 mptnn0fsupp 13964 mptnn0fsuppr 13966 fsumzcl2 15687 fsummsnunz 15702 fsumsplitsnun 15703 modfsummodslem1 15740 fprodmodd 15943 sumeven 16332 sumodd 16333 gsummpt1n0 19835 gsummptnn0fz 19856 telgsumfzslem 19858 telgsumfzs 19859 telgsums 19863 mptscmfsupp0 20542 coe1fzgsumdlem 21832 gsummoncoe1 21835 evl1gsumdlem 21882 madugsum 22152 iunmbl2 25081 gsumvsca1 32412 gsumvsca2 32413 rmfsupp2 32428 esum2dlem 33159 esumiun 33161 f1o2d2 41141 iblsplitf 44765 fsummsndifre 46119 fsumsplitsndif 46120 fsummmodsndifre 46121 fsummmodsnunz 46122 |
Copyright terms: Public domain | W3C validator |