![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sslin | Structured version Visualization version GIF version |
Description: Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.) |
Ref | Expression |
---|---|
sslin | ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssrin 4064 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | |
2 | incom 4034 | . 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) | |
3 | incom 4034 | . 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶) | |
4 | 1, 2, 3 | 3sstr4g 3871 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∩ cin 3797 ⊆ wss 3798 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-v 3416 df-in 3805 df-ss 3812 |
This theorem is referenced by: ss2in 4067 inxpssres 5363 ssres2 5665 sbthlem7 8351 kmlem5 9298 canthnum 9793 ioodisj 12602 hashun3 13470 xpsc0 16580 dprdres 18788 dprd2da 18802 dmdprdsplit2lem 18805 cnprest 21471 isnrm3 21541 regsep2 21558 llycmpkgen2 21731 kqdisj 21913 regr1lem 21920 fclsbas 22202 fclscf 22206 flimfnfcls 22209 isfcf 22215 metdstri 23031 nulmbl2 23709 uniioombllem4 23759 volsup2 23778 volcn 23779 itg1climres 23887 limcresi 24055 limciun 24064 rlimcnp2 25113 rplogsum 25636 chssoc 28906 cmbr4i 29011 5oai 29071 3oalem6 29077 mdslmd4i 29743 atcvat4i 29807 imadifxp 29957 crefss 30457 pnfneige0 30538 cldbnd 32854 neibastop1 32887 neibastop2 32889 onint1 32976 oninhaus 32977 cntotbnd 34132 polcon3N 35987 osumcllem4N 36029 lcfrlem2 37613 mapfzcons1 38119 coeq0i 38155 eldioph4b 38214 icccncfext 40889 srhmsubc 42937 fldc 42944 fldhmsubc 42945 rhmsubclem3 42949 srhmsubcALTV 42955 fldcALTV 42962 fldhmsubcALTV 42963 rhmsubcALTVlem4 42968 |
Copyright terms: Public domain | W3C validator |