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 4167 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | |
2 | incom 4135 | . 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) | |
3 | incom 4135 | . 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶) | |
4 | 1, 2, 3 | 3sstr4g 3966 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∩ cin 3886 ⊆ wss 3887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-in 3894 df-ss 3904 |
This theorem is referenced by: ss2in 4170 inxpssres 5606 ssres2 5919 predrelss 6240 sbthlem7 8876 kmlem5 9910 canthnum 10405 ioodisj 13214 hashun3 14099 dprdres 19631 dprd2da 19645 dmdprdsplit2lem 19648 cnprest 22440 isnrm3 22510 regsep2 22527 llycmpkgen2 22701 kqdisj 22883 regr1lem 22890 fclsbas 23172 fclscf 23176 flimfnfcls 23179 isfcf 23185 metdstri 24014 nulmbl2 24700 uniioombllem4 24750 volsup2 24769 volcn 24770 itg1climres 24879 limcresi 25049 limciun 25058 rlimcnp2 26116 rplogsum 26675 chssoc 29858 cmbr4i 29963 5oai 30023 3oalem6 30029 mdslmd4i 30695 atcvat4i 30759 imadifxp 30940 swrdrndisj 31229 crefss 31799 pnfneige0 31901 cldbnd 34515 neibastop1 34548 neibastop2 34550 onint1 34638 oninhaus 34639 bj-idres 35331 cntotbnd 35954 polcon3N 37931 osumcllem4N 37973 lcfrlem2 39557 mapfzcons1 40539 coeq0i 40575 eldioph4b 40633 icccncfext 43428 srhmsubc 45634 fldc 45641 fldhmsubc 45642 rhmsubclem3 45646 srhmsubcALTV 45652 fldcALTV 45659 fldhmsubcALTV 45660 rhmsubcALTVlem4 45665 ssdisjdr 46154 sepnsepolem2 46216 |
Copyright terms: Public domain | W3C validator |