![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sstr2 | Structured version Visualization version Unicode version |
Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Ref | Expression |
---|---|
sstr2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3438 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | imim1d 78 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | alimdv 1774 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | dfss2 3433 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | dfss2 3433 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3imtr4g 278 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-in 3423 df-ss 3430 |
This theorem is referenced by: sstr 3452 sstri 3453 sseq1 3465 sseq2 3466 ssun3 3611 ssun4 3612 ssinss1 3672 ssdisj 3826 triun 4524 trint0 4528 sspwb 4663 exss 4677 frss 4820 relss 4941 funss 5619 funimass2 5679 fss 5760 suceloni 6667 limsssuc 6704 oaordi 7273 oeworde 7320 nnaordi 7345 sbthlem2 7709 sbthlem3 7710 sbthlem6 7713 domunfican 7870 fiint 7874 fiss 7964 dffi3 7971 inf3lem1 8159 trcl 8238 tcss 8254 ac10ct 8491 ackbij2lem4 8698 cfslb 8722 cfslbn 8723 cfcoflem 8728 coftr 8729 fin23lem15 8790 fin23lem20 8793 fin23lem36 8804 isf32lem1 8809 axdc3lem2 8907 ttukeylem2 8966 wunex2 9189 tskcard 9232 clsslem 13097 mrcss 15571 isacs2 15608 lubss 16416 frmdss2 16696 lsmlub 17364 lsslss 18233 lspss 18256 aspss 18605 mplcoe1 18738 mplcoe5 18741 ocv2ss 19285 ocvsscon 19287 lindsss 19431 lsslinds 19438 mdetunilem9 19694 tgss 20033 tgcl 20034 tgss3 20051 clsss 20118 ntrss 20119 neiss 20174 ssnei2 20181 opnnei 20185 cnpnei 20329 cnpco 20332 cncls 20339 cnprest 20354 hauscmp 20471 1stcfb 20509 1stcelcls 20525 reftr 20578 txcnpi 20672 txcnp 20684 txtube 20704 qtoptop2 20763 fgcl 20942 filssufilg 20975 ufileu 20983 uffix 20985 elfm2 21012 fmfnfmlem1 21018 fmco 21025 fbflim2 21041 flffbas 21059 flftg 21060 cnpflf2 21064 alexsubALTlem4 21114 neibl 21565 metcnp3 21604 xlebnum 22045 lebnumii 22046 caubl 22326 caublcls 22327 bcthlem2 22342 bcthlem5 22345 ovolsslem 22486 volsuplem 22557 dyadmbllem 22606 ellimc3 22883 limciun 22898 cpnord 22938 ubthlem1 26561 occon3 26999 chsupval 27037 chsupcl 27042 chsupss 27044 spanss 27050 chsupval2 27112 stlei 27942 dmdbr5 28010 mdsl0 28012 chrelat2i 28067 chirredlem1 28092 mdsymlem5 28109 mdsymlem6 28110 gsumle 28591 gsumvsca1 28594 gsumvsca2 28595 omsmon 29175 omsmonOLD 29179 cvmliftlem15 30070 ss2mcls 30255 mclsax 30256 clsint2 31034 fgmin 31075 filnetlem4 31086 limsucncmpi 31154 ptrecube 31985 heiborlem1 32188 heiborlem8 32195 pclssN 33504 dochexmidlem7 35079 incssnn0 35598 islssfg2 35974 hbtlem6 36033 hess 36420 psshepw 36429 sspwimpcf 37357 sspwimpcfVD 37358 dvmptfprod 37858 elbigo2 40636 |
Copyright terms: Public domain | W3C validator |