![]() |
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 8070 mptnn0fsupp 13961 mptnn0fsuppr 13963 fsumzcl2 15684 fsummsnunz 15699 fsumsplitsnun 15700 modfsummodslem1 15737 fprodmodd 15940 sumeven 16329 sumodd 16330 gsummpt1n0 19832 gsummptnn0fz 19853 telgsumfzslem 19855 telgsumfzs 19856 telgsums 19860 mptscmfsupp0 20536 coe1fzgsumdlem 21824 gsummoncoe1 21827 evl1gsumdlem 21874 madugsum 22144 iunmbl2 25073 gsumvsca1 32366 gsumvsca2 32367 rmfsupp2 32382 esum2dlem 33085 esumiun 33087 f1o2d2 41057 iblsplitf 44676 fsummsndifre 46030 fsumsplitsndif 46031 fsummmodsndifre 46032 fsummmodsnunz 46033 |
Copyright terms: Public domain | W3C validator |