![]() |
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 3985 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | |
2 | 1 | imp 407 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ⊆ wss 3944 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3951 df-ss 3961 |
This theorem is referenced by: sstrd 3988 sylan9ss 3991 ssdifss 4131 uneqin 4274 intss2 5104 ssrnres 6166 relrelss 6261 fcof 6727 fcoOLD 6729 fssres 6744 ssimaex 6962 dff3 7086 tpostpos2 8214 smores 8334 om00 8558 omeulem2 8566 cofonr 8656 naddunif 8675 pmss12g 8846 unblem1 9278 unblem2 9279 unblem3 9280 unblem4 9281 isfinite2 9284 cantnfval2 9646 cantnfle 9648 rankxplim3 9858 alephinit 10072 dfac12lem2 10121 ackbij1lem11 10207 cfeq0 10233 cfsuc 10234 cff1 10235 cflim2 10240 cfss 10242 cfslb2n 10245 cofsmo 10246 cfsmolem 10247 fin23lem34 10323 fin1a2lem13 10389 axdc3lem2 10428 axdclem 10496 pwcfsdom 10560 wunfi 10698 tskxpss 10749 tskcard 10758 suprzcl 12624 uzwo 12877 uzwo2 12878 infssuzle 12897 infssuzcl 12898 supxrbnd 13289 supxrgtmnf 13290 supxrre1 13291 supxrre2 13292 supxrss 13293 infxrss 13300 iccsupr 13401 hashf1lem2 14399 trclun 14943 fsum2d 15699 fsumabs 15729 fsumrlim 15739 fsumo1 15740 fprod2d 15907 rpnnen2lem4 16142 rpnnen2lem7 16145 ramub2 16929 ressinbas 17172 ressress 17175 submre 17531 mrcss 17542 mreacs 17584 drsdirfi 18240 clatglbss 18454 ipopos 18471 cntz2ss 19163 pgrpsubgsymg 19241 ablfac1eulem 19901 subrgint 20335 tgval 22387 mretopd 22525 ssnei 22543 opnneiss 22551 restdis 22611 restcls 22614 restntr 22615 tgcnp 22686 fbssfi 23270 fgss2 23307 fgcl 23311 supfil 23328 alexsubALTlem3 23482 alexsubALTlem4 23483 cnextcn 23500 ustex3sym 23651 trust 23663 restutop 23671 utop2nei 23684 cfiluweak 23729 blssexps 23861 blssex 23862 mopni3 23932 metss 23946 metcnp3 23978 metust 23996 cfilucfil 23997 psmetutop 24005 tgioo 24241 xrsmopn 24257 fsumcn 24315 cncfmptid 24358 iscmet3lem2 24738 caussi 24743 ovolsslem 24930 ovolsscl 24932 ovolssnul 24933 opnmblALT 25049 itgfsum 25273 limcresi 25331 dvmptfsum 25421 plyss 25642 madebdayim 27305 cofcutrtime 27334 nbuhgr 28465 chsupunss 30460 shsupunss 30462 spanss 30464 shslubi 30501 shlub 30530 mdsl1i 31437 mdsl2i 31438 cvmdi 31440 mdslmd1lem1 31441 mdslmd1lem2 31442 mdslmd2i 31446 mdslmd4i 31449 atomli 31498 atcvatlem 31501 chirredlem2 31507 chirredi 31510 mdsymlem5 31523 xrge0infss 31844 tpr2rico 32723 sigainb 32965 dya2icoseg2 33108 omssubadd 33130 eulerpartlemn 33211 ballotlem2 33318 nummin 33925 cvmlift2lem12 34136 opnbnd 35014 fneint 35037 dissneqlem 36025 inunissunidif 36060 pibt2 36102 fin2so 36279 matunitlindflem1 36288 mblfinlem4 36332 ismblfin 36333 filbcmb 36413 heiborlem10 36493 igenmin 36737 lssatle 37690 paddss1 38493 paddss2 38494 paddss12 38495 paddssw2 38520 pclssN 38570 pclfinN 38576 polsubN 38583 2polvalN 38590 2polssN 38591 3polN 38592 2pmaplubN 38602 pnonsingN 38609 polsubclN 38628 dihord6apre 39932 dochsscl 40044 mapdordlem2 40313 isnacs3 41219 itgoss 41676 ofoaid1 41879 ofoaid2 41880 sspwimp 43450 sspwimpVD 43451 nsstr 43555 islptre 44108 gsumlsscl 46707 lincellss 46755 ellcoellss 46764 |
Copyright terms: Public domain | W3C validator |