| 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 4242 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∩ cin 3950 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-in 3958 df-ss 3968 |
| This theorem is referenced by: fictb 10284 isacs1i 17700 rescabs 17877 rescabsOLD 17878 lsmdisj 19699 dmdprdsplit2lem 20065 rhmsscrnghm 20665 rngcresringcat 20669 acsfn1p 20800 obselocv 21748 restbas 23166 neitr 23188 restcls 23189 restntr 23190 nrmsep 23365 cldllycmp 23503 fclsneii 24025 tsmsres 24152 trcfilu 24303 metdseq0 24876 iundisj2 25584 uniioombllem3 25620 ppisval 27147 ppisval2 27148 chtwordi 27199 ppiwordi 27205 chpub 27264 chebbnd1lem1 27513 mdbr2 32315 mdslj1i 32338 mdsl2i 32341 mdslmd1lem1 32344 mdslmd3i 32351 mdexchi 32354 sumdmdlem 32437 iundisj2f 32603 iundisj2fi 32799 cycpmco2f1 33144 tocyccntz 33164 esumrnmpt2 34069 bnj1177 35020 sstotbnd2 37781 lcvexchlem5 39039 pnonsingN 39935 dochnoncon 41393 eldioph2lem2 42772 limsupres 45720 limsupresxr 45781 liminfresxr 45782 liminflelimsuplem 45790 ssdisjd 48727 |
| Copyright terms: Public domain | W3C validator |