| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sstr | Structured version Visualization version GIF version | ||
| Description: Transitivity of subclass relationship. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.) |
| Ref | Expression |
|---|---|
| sstr | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sstr2 3990 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | |
| 2 | 1 | imp 406 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ⊆ 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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ss 3968 |
| This theorem is referenced by: sstrd 3994 sylan9ss 3997 ssdifss 4140 uneqin 4289 intss2 5108 ssrnres 6198 relrelss 6293 fcof 6759 fssres 6774 ssimaex 6994 dff3 7120 tpostpos2 8272 smores 8392 om00 8613 omeulem2 8621 cofonr 8712 naddunif 8731 pmss12g 8909 unblem1 9328 unblem2 9329 unblem3 9330 unblem4 9331 isfinite2 9334 cantnfval2 9709 cantnfle 9711 rankxplim3 9921 alephinit 10135 dfac12lem2 10185 ackbij1lem11 10269 cfeq0 10296 cfsuc 10297 cff1 10298 cflim2 10303 cfss 10305 cfslb2n 10308 cofsmo 10309 cfsmolem 10310 fin23lem34 10386 fin1a2lem13 10452 axdc3lem2 10491 axdclem 10559 pwcfsdom 10623 wunfi 10761 tskxpss 10812 tskcard 10821 suprzcl 12698 uzwo 12953 uzwo2 12954 infssuzle 12973 infssuzcl 12974 supxrbnd 13370 supxrgtmnf 13371 supxrre1 13372 supxrre2 13373 supxrss 13374 infxrss 13381 iccsupr 13482 hashf1lem2 14495 trclun 15053 fsum2d 15807 fsumabs 15837 fsumrlim 15847 fsumo1 15848 fprod2d 16017 rpnnen2lem4 16253 rpnnen2lem7 16256 ramub2 17052 ressinbas 17291 ressress 17293 submre 17648 mrcss 17659 mreacs 17701 drsdirfi 18351 clatglbss 18564 ipopos 18581 cntz2ss 19353 pgrpsubgsymg 19427 ablfac1eulem 20092 subrngint 20560 subrgint 20595 tgval 22962 mretopd 23100 ssnei 23118 opnneiss 23126 restdis 23186 restcls 23189 restntr 23190 tgcnp 23261 fbssfi 23845 fgss2 23882 fgcl 23886 supfil 23903 alexsubALTlem3 24057 alexsubALTlem4 24058 cnextcn 24075 ustex3sym 24226 trust 24238 restutop 24246 utop2nei 24259 cfiluweak 24304 blssexps 24436 blssex 24437 mopni3 24507 metss 24521 metcnp3 24553 metust 24571 cfilucfil 24572 psmetutop 24580 tgioo 24817 xrsmopn 24834 fsumcn 24894 cncfmptid 24939 iscmet3lem2 25326 caussi 25331 ovolsslem 25519 ovolsscl 25521 ovolssnul 25522 opnmblALT 25638 itgfsum 25862 limcresi 25920 dvmptfsum 26013 plyss 26238 madebdayim 27926 cofcutrtime 27961 nbuhgr 29360 chsupunss 31363 shsupunss 31365 spanss 31367 shslubi 31404 shlub 31433 mdsl1i 32340 mdsl2i 32341 cvmdi 32343 mdslmd1lem1 32344 mdslmd1lem2 32345 mdslmd2i 32349 mdslmd4i 32352 atomli 32401 atcvatlem 32404 chirredlem2 32410 chirredi 32413 mdsymlem5 32426 xrge0infss 32764 tpr2rico 33911 sigainb 34137 dya2icoseg2 34280 omssubadd 34302 eulerpartlemn 34383 ballotlem2 34491 nummin 35105 cvmlift2lem12 35319 opnbnd 36326 fneint 36349 dissneqlem 37341 inunissunidif 37376 pibt2 37418 fin2so 37614 matunitlindflem1 37623 mblfinlem4 37667 ismblfin 37668 filbcmb 37747 heiborlem10 37827 igenmin 38071 lssatle 39016 paddss1 39819 paddss2 39820 paddss12 39821 paddssw2 39846 pclssN 39896 pclfinN 39902 polsubN 39909 2polvalN 39916 2polssN 39917 3polN 39918 2pmaplubN 39928 pnonsingN 39935 polsubclN 39954 dihord6apre 41258 dochsscl 41370 mapdordlem2 41639 isnacs3 42721 itgoss 43175 ofoaid1 43371 ofoaid2 43372 sspwimp 44938 sspwimpVD 44939 nsstr 45100 islptre 45634 gsumlsscl 48296 lincellss 48343 ellcoellss 48352 |
| Copyright terms: Public domain | W3C validator |