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 4207 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | |
2 | incom 4175 | . 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) | |
3 | incom 4175 | . 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶) | |
4 | 1, 2, 3 | 3sstr4g 4009 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∩ cin 3932 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-in 3940 df-ss 3949 |
This theorem is referenced by: ss2in 4210 inxpssres 5565 ssres2 5874 sbthlem7 8621 kmlem5 9568 canthnum 10059 ioodisj 12856 hashun3 13733 dprdres 19079 dprd2da 19093 dmdprdsplit2lem 19096 cnprest 21825 isnrm3 21895 regsep2 21912 llycmpkgen2 22086 kqdisj 22268 regr1lem 22275 fclsbas 22557 fclscf 22561 flimfnfcls 22564 isfcf 22570 metdstri 23386 nulmbl2 24064 uniioombllem4 24114 volsup2 24133 volcn 24134 itg1climres 24242 limcresi 24410 limciun 24419 rlimcnp2 25471 rplogsum 26030 chssoc 29200 cmbr4i 29305 5oai 29365 3oalem6 29371 mdslmd4i 30037 atcvat4i 30101 imadifxp 30279 swrdrndisj 30558 crefss 31012 pnfneige0 31093 cldbnd 33571 neibastop1 33604 neibastop2 33606 onint1 33694 oninhaus 33695 bj-idres 34344 cntotbnd 34955 polcon3N 36933 osumcllem4N 36975 lcfrlem2 38559 mapfzcons1 39192 coeq0i 39228 eldioph4b 39286 icccncfext 42046 srhmsubc 44275 fldc 44282 fldhmsubc 44283 rhmsubclem3 44287 srhmsubcALTV 44293 fldcALTV 44300 fldhmsubcALTV 44301 rhmsubcALTVlem4 44306 |
Copyright terms: Public domain | W3C validator |