Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssrind | Structured version Visualization version GIF version |
Description: Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
Ref | Expression |
---|---|
ssrind.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Ref | Expression |
---|---|
ssrind | ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssrind.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | ssrin 4207 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | |
3 | 1, 2 | syl 17 | 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-v 3494 df-in 3940 df-ss 3949 |
This theorem is referenced by: fictb 9655 isacs1i 16916 rescabs 17091 lsmdisj 18736 dmdprdsplit2lem 19096 acsfn1p 19507 obselocv 20800 restbas 21694 neitr 21716 restcls 21717 restntr 21718 nrmsep 21893 cldllycmp 22031 fclsneii 22553 tsmsres 22679 trcfilu 22830 metdseq0 23389 iundisj2 24077 uniioombllem3 24113 ppisval 25608 ppisval2 25609 chtwordi 25660 ppiwordi 25666 chpub 25723 chebbnd1lem1 25972 mdbr2 30000 mdslj1i 30023 mdsl2i 30026 mdslmd1lem1 30029 mdslmd3i 30036 mdexchi 30039 sumdmdlem 30122 iundisj2f 30268 iundisj2fi 30446 cycpmco2f1 30693 tocyccntz 30713 esumrnmpt2 31226 bnj1177 32175 sstotbnd2 34933 lcvexchlem5 36054 pnonsingN 36949 dochnoncon 38407 eldioph2lem2 39236 limsupres 41862 limsupresxr 41923 liminfresxr 41924 liminflelimsuplem 41932 rhmsscrnghm 44225 rngcresringcat 44229 |
Copyright terms: Public domain | W3C validator |