![]() |
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 3630 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 587 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
3 | elin 3829 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)) | |
4 | elin 3829 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | |
5 | 2, 3, 4 | 3imtr4g 285 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶))) |
6 | 5 | ssrdv 3642 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2030 ∩ cin 3606 ⊆ wss 3607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-in 3614 df-ss 3621 |
This theorem is referenced by: sslin 3872 ss2in 3873 ssdisj 4059 ssdisjOLD 4060 ssdifin0 4083 ssres 5459 predpredss 5724 sbthlem7 8117 onsdominel 8150 phplem2 8181 infdifsn 8592 fictb 9105 fin23lem23 9186 ttukeylem2 9370 limsupgord 14247 xpsc1 16268 isacs1i 16365 rescabs 16540 lsmdisj 18140 dmdprdsplit2lem 18490 pjfval 20098 pjpm 20100 obselocv 20120 tgss 20820 neindisj2 20975 restbas 21010 neitr 21032 restcls 21033 restntr 21034 nrmsep 21209 1stcrest 21304 cldllycmp 21346 kgencn3 21409 trfbas2 21694 fclsneii 21868 fclsrest 21875 fcfnei 21886 cnextcn 21918 tsmsres 21994 trust 22080 restutopopn 22089 trcfilu 22145 metrest 22376 reperflem 22668 metdseq0 22704 iundisj2 23363 uniioombllem3 23399 ellimc3 23688 limcflf 23690 lhop1lem 23821 ppisval 24875 ppisval2 24876 ppinprm 24923 chtnprm 24925 chtwordi 24927 ppiwordi 24933 chpub 24990 chebbnd1lem1 25203 chtppilimlem1 25207 orthin 28433 3oalem6 28654 mdbr2 29283 mdslle1i 29304 mdslle2i 29305 mdslj1i 29306 mdslj2i 29307 mdsl2i 29309 mdslmd1lem1 29312 mdslmd1lem2 29313 mdslmd3i 29319 mdexchi 29322 sumdmdlem 29405 iundisj2f 29529 iundisj2fi 29684 esumrnmpt2 30258 eulerpartlemn 30571 bnj1177 31200 poimirlem3 33542 poimirlem29 33568 ismblfin 33580 sstotbnd2 33703 lcvexchlem5 34643 pnonsingN 35537 dochnoncon 36997 eldioph2lem2 37641 acsfn1p 38086 ssrind 39647 nnuzdisj 39884 sumnnodd 40180 limsupres 40255 liminfgord 40304 sge0less 40927 rhmsscrnghm 42351 rngcresringcat 42355 |
Copyright terms: Public domain | W3C validator |