Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssrin | Structured version Visualization version GIF version |
Description: Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
ssrin | ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3893 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 614 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
3 | elin 3882 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)) | |
4 | elin 3882 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | |
5 | 2, 3, 4 | 3imtr4g 299 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶))) |
6 | 5 | ssrdv 3907 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2110 ∩ cin 3865 ⊆ wss 3866 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-in 3873 df-ss 3883 |
This theorem is referenced by: sslin 4149 ssrind 4150 ss2in 4151 ssdisj 4374 ssdifin0 4397 ssres 5878 predpredss 6166 sbthlem7 8762 onsdominel 8795 phplem2 8826 infdifsn 9272 fin23lem23 9940 ttukeylem2 10124 limsupgord 15033 pjfval 20668 pjpm 20670 tgss 21865 neindisj2 22020 1stcrest 22350 kgencn3 22455 trfbas2 22740 fclsrest 22921 fcfnei 22932 cnextcn 22964 tsmsres 23041 trust 23127 restutopopn 23136 metrest 23422 reperflem 23715 ellimc3 24776 limcflf 24778 lhop1lem 24910 ppinprm 26034 chtnprm 26036 chtppilimlem1 26354 orthin 29527 3oalem6 29748 mdslle1i 30398 mdslle2i 30399 mdslj1i 30400 mdslj2i 30401 mdslmd1lem2 30407 mdslmd3i 30413 mdexchi 30416 eulerpartlemn 32060 poimirlem3 35517 poimirlem29 35543 ismblfin 35555 nnuzdisj 42567 sumnnodd 42846 liminfgord 42970 sge0less 43605 sepnsepo 45890 |
Copyright terms: Public domain | W3C validator |