| 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 3977 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
| 2 | 1 | anim1d 611 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
| 3 | elin 3967 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)) | |
| 4 | elin 3967 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | |
| 5 | 2, 3, 4 | 3imtr4g 296 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶))) |
| 6 | 5 | ssrdv 3989 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ∩ 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: sslin 4243 ssrind 4244 ss2in 4245 ssdisj 4460 ssdifin0 4486 ssres 6021 predpredss 6328 sbthlem7 9129 onsdominel 9166 phplem2OLD 9255 infdifsn 9697 fin23lem23 10366 ttukeylem2 10550 limsupgord 15508 pjfval 21726 pjpm 21728 tgss 22975 neindisj2 23131 1stcrest 23461 kgencn3 23566 trfbas2 23851 fclsrest 24032 fcfnei 24043 cnextcn 24075 tsmsres 24152 trust 24238 restutopopn 24247 metrest 24537 reperflem 24840 ellimc3 25914 limcflf 25916 lhop1lem 26052 ppinprm 27195 chtnprm 27197 chtppilimlem1 27517 orthin 31465 3oalem6 31686 mdslle1i 32336 mdslle2i 32337 mdslj1i 32338 mdslj2i 32339 mdslmd1lem2 32345 mdslmd3i 32351 mdexchi 32354 eulerpartlemn 34383 poimirlem3 37630 poimirlem29 37656 ismblfin 37668 nnuzdisj 45366 sumnnodd 45645 liminfgord 45769 sge0less 46407 sepnsepo 48821 |
| Copyright terms: Public domain | W3C validator |