| 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 4196 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | |
| 3 | 1, 2 | syl 18 | 1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∩ cin 3906 ⊆ wss 3907 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-tru 1566 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-v 3459 df-in 3914 df-ss 3924 |
| This theorem is referenced by: fictb 10215 isacs1i 17701 rescabs 17878 lsmdisj 19739 dmdprdsplit2lem 20105 rhmsscrnghm 20738 rngcresringcat 20742 acsfn1p 20868 obselocv 21835 restbas 23272 neitr 23294 restcls 23295 restntr 23296 nrmsep 23471 cldllycmp 23609 fclsneii 24131 tsmsres 24258 trcfilu 24407 metdseq0 24969 iundisj2 25665 uniioombllem3 25701 ppisval 27222 ppisval2 27223 chtwordi 27274 ppiwordi 27280 chpub 27338 chebbnd1lem1 27587 mdbr2 32553 mdslj1i 32576 mdsl2i 32579 mdslmd1lem1 32582 mdslmd3i 32589 mdexchi 32592 sumdmdlem 32675 iundisj2f 32841 iundisj2fi 33050 cycpmco2f1 33352 tocyccntz 33372 esumrnmpt2 34370 bnj1177 35306 sstotbnd2 38280 lcvexchlem5 39669 pnonsingN 40564 dochnoncon 42022 eldioph2lem2 43349 limsupres 46278 limsupresxr 46339 liminfresxr 46340 liminflelimsuplem 46348 ssdisjd 49438 |
| Copyright terms: Public domain | W3C validator |