![]() |
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 4233 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | |
2 | incom 4201 | . 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) | |
3 | incom 4201 | . 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶) | |
4 | 1, 2, 3 | 3sstr4g 4027 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∩ cin 3947 ⊆ wss 3948 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-in 3955 df-ss 3965 |
This theorem is referenced by: ss2in 4236 inxpssres 5693 ssres2 6009 predrelss 6338 sbthlem7 9095 kmlem5 10155 canthnum 10650 ioodisj 13466 hashun3 14351 dprdres 19946 dprd2da 19960 dmdprdsplit2lem 19963 srhmsubc 20572 rhmsubclem3 20579 fldc 20631 fldhmsubc 20632 cnprest 23113 isnrm3 23183 regsep2 23200 llycmpkgen2 23374 kqdisj 23556 regr1lem 23563 fclsbas 23845 fclscf 23849 flimfnfcls 23852 isfcf 23858 metdstri 24687 nulmbl2 25385 uniioombllem4 25435 volsup2 25454 volcn 25455 itg1climres 25564 limcresi 25734 limciun 25743 rlimcnp2 26812 rplogsum 27373 chssoc 31182 cmbr4i 31287 5oai 31347 3oalem6 31353 mdslmd4i 32019 atcvat4i 32083 imadifxp 32265 swrdrndisj 32554 crefss 33293 pnfneige0 33395 cldbnd 35675 neibastop1 35708 neibastop2 35710 onint1 35798 oninhaus 35799 bj-idres 36505 cntotbnd 37128 polcon3N 39252 osumcllem4N 39294 lcfrlem2 40878 mapfzcons1 41918 coeq0i 41954 eldioph4b 42012 icccncfext 45062 rhmsubcALTVlem4 47121 srhmsubcALTV 47162 fldcALTV 47169 fldhmsubcALTV 47170 ssdisjdr 47655 sepnsepolem2 47717 |
Copyright terms: Public domain | W3C validator |