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 4124 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | |
2 | incom 4091 | . 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) | |
3 | incom 4091 | . 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶) | |
4 | 1, 2, 3 | 3sstr4g 3922 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∩ cin 3842 ⊆ wss 3843 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-rab 3062 df-v 3400 df-in 3850 df-ss 3860 |
This theorem is referenced by: ss2in 4127 inxpssres 5542 ssres2 5853 sbthlem7 8685 kmlem5 9656 canthnum 10151 ioodisj 12958 hashun3 13839 dprdres 19271 dprd2da 19285 dmdprdsplit2lem 19288 cnprest 22042 isnrm3 22112 regsep2 22129 llycmpkgen2 22303 kqdisj 22485 regr1lem 22492 fclsbas 22774 fclscf 22778 flimfnfcls 22781 isfcf 22787 metdstri 23605 nulmbl2 24290 uniioombllem4 24340 volsup2 24359 volcn 24360 itg1climres 24469 limcresi 24639 limciun 24648 rlimcnp2 25706 rplogsum 26265 chssoc 29433 cmbr4i 29538 5oai 29598 3oalem6 29604 mdslmd4i 30270 atcvat4i 30334 imadifxp 30516 swrdrndisj 30806 crefss 31373 pnfneige0 31475 cldbnd 34160 neibastop1 34193 neibastop2 34195 onint1 34283 oninhaus 34284 bj-idres 34974 cntotbnd 35599 polcon3N 37576 osumcllem4N 37618 lcfrlem2 39202 mapfzcons1 40133 coeq0i 40169 eldioph4b 40227 icccncfext 42992 srhmsubc 45197 fldc 45204 fldhmsubc 45205 rhmsubclem3 45209 srhmsubcALTV 45215 fldcALTV 45222 fldhmsubcALTV 45223 rhmsubcALTVlem4 45228 ssdisjdr 45715 sepnsepolem2 45767 |
Copyright terms: Public domain | W3C validator |