![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssrin | Structured version Visualization version Unicode 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 3437 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anim1d 572 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | elin 3628 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | elin 3628 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3imtr4g 278 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | ssrdv 3449 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-v 3058 df-in 3422 df-ss 3429 |
This theorem is referenced by: sslin 3669 ss2in 3670 ssdisj 3825 ssdifin0 3860 ssres 5148 predpredss 5404 sbthlem7 7713 onsdominel 7746 phplem2 7777 infdifsn 8187 fictb 8700 fin23lem23 8781 ttukeylem2 8965 limsupgord 13576 xpsc1 15515 isacs1i 15611 rescabs 15786 lsmdisj 17379 dmdprdsplit2lem 17726 pjfval 19317 pjpm 19319 obselocv 19339 tgss 20032 neindisj2 20187 restbas 20222 neitr 20244 restcls 20245 restntr 20246 nrmsep 20421 1stcrest 20516 cldllycmp 20558 kgencn3 20621 trfbas2 20906 fclsneii 21080 fclsrest 21087 fcfnei 21098 cnextcn 21130 tsmsres 21206 trust 21292 restutopopn 21301 trcfilu 21357 metrest 21587 reperflem 21884 metdseq0 21919 metdseq0OLD 21934 iundisj2 22550 uniioombllem3 22591 ellimc3 22882 limcflf 22884 lhop1lem 23013 ppisval 24078 ppisval2 24079 ppinprm 24127 chtnprm 24129 chtwordi 24131 ppiwordi 24137 chpub 24196 chebbnd1lem1 24355 chtppilimlem1 24359 orthin 27147 3oalem6 27368 mdbr2 27997 mdslle1i 28018 mdslle2i 28019 mdslj1i 28020 mdslj2i 28021 mdsl2i 28023 mdslmd1lem1 28026 mdslmd1lem2 28027 mdslmd3i 28033 mdexchi 28036 sumdmdlem 28119 iundisj2f 28248 iundisj2fi 28421 esumrnmpt2 28937 eulerpartlemn 29262 bnj1177 29863 poimirlem3 31987 poimirlem29 32013 ismblfin 32025 sstotbnd2 32150 lcvexchlem5 32648 pnonsingN 33542 dochnoncon 35003 eldioph2lem2 35647 acsfn1p 36109 nnuzdisj 37615 sumnnodd 37747 sge0less 38271 rhmsscrnghm 40300 rngcresringcat 40304 |
Copyright terms: Public domain | W3C validator |