![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sstr | Structured version Visualization version GIF version |
Description: Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.) |
Ref | Expression |
---|---|
sstr | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstr2 3643 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | |
2 | 1 | imp 444 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ⊆ 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-in 3614 df-ss 3621 |
This theorem is referenced by: sstrd 3646 sylan9ss 3649 ssdifss 3774 uneqin 3911 ssrnres 5607 relrelss 5697 fco 6096 fssres 6108 ssimaex 6302 dff3 6412 tpostpos2 7418 smores 7494 om00 7700 omeulem2 7708 pmss12g 7926 unblem1 8253 unblem2 8254 unblem3 8255 unblem4 8256 isfinite2 8259 cantnfval2 8604 cantnfle 8606 rankxplim3 8782 alephinit 8956 dfac12lem2 9004 ackbij1lem11 9090 cfeq0 9116 cfsuc 9117 cff1 9118 cflim2 9123 cfss 9125 cfslb2n 9128 cofsmo 9129 cfsmolem 9130 fin23lem34 9206 fin1a2lem13 9272 axdc3lem2 9311 axdclem 9379 pwcfsdom 9443 wunfi 9581 tskxpss 9632 tskcard 9641 suprzcl 11495 uzwo 11789 uzwo2 11790 infssuzle 11809 infssuzcl 11810 supxrbnd 12196 supxrgtmnf 12197 supxrre1 12198 supxrre2 12199 supxrss 12200 infxrss 12207 iccsupr 12304 hashf1lem2 13278 trclun 13799 fsum2d 14546 fsumabs 14577 fsumrlim 14587 fsumo1 14588 fprod2d 14755 rpnnen2lem4 14990 rpnnen2lem7 14993 ramub2 15765 ressinbas 15983 ressress 15985 submre 16312 mrcss 16323 mreacs 16366 drsdirfi 16985 clatglbss 17174 ipopos 17207 cntz2ss 17811 ablfac1eulem 18517 subrgint 18850 tgval 20807 mretopd 20944 ssnei 20962 opnneiss 20970 restdis 21030 restcls 21033 restntr 21034 tgcnp 21105 fbssfi 21688 fgss2 21725 fgcl 21729 supfil 21746 alexsubALTlem3 21900 alexsubALTlem4 21901 cnextcn 21918 ustex3sym 22068 trust 22080 restutop 22088 utop2nei 22101 cfiluweak 22146 blssexps 22278 blssex 22279 mopni3 22346 metss 22360 metcnp3 22392 metust 22410 cfilucfil 22411 psmetutop 22419 tgioo 22646 xrsmopn 22662 fsumcn 22720 cncfmptid 22762 iscmet3lem2 23136 caussi 23141 ovolsslem 23298 ovolsscl 23300 ovolssnul 23301 opnmblALT 23417 itgfsum 23638 limcresi 23694 dvmptfsum 23783 plyss 24000 nbuhgr 26284 chsupunss 28331 shsupunss 28333 spanss 28335 shslubi 28372 shlub 28401 mdsl1i 29308 mdsl2i 29309 cvmdi 29311 mdslmd1lem1 29312 mdslmd1lem2 29313 mdslmd2i 29317 mdslmd4i 29320 atomli 29369 atcvatlem 29372 chirredlem2 29378 chirredi 29381 mdsymlem5 29394 xrge0infss 29653 tpr2rico 30086 sigainb 30327 dya2icoseg2 30468 omssubadd 30490 eulerpartlemn 30571 ballotlem2 30678 cvmlift2lem12 31422 opnbnd 32445 fneint 32468 bj-intss 33178 dissneqlem 33317 fin2so 33526 matunitlindflem1 33535 mblfinlem4 33579 ismblfin 33580 filbcmb 33665 heiborlem10 33749 igenmin 33993 lssatle 34620 paddss1 35421 paddss2 35422 paddss12 35423 paddssw2 35448 pclssN 35498 pclfinN 35504 polsubN 35511 2polvalN 35518 2polssN 35519 3polN 35520 2pmaplubN 35530 pnonsingN 35537 polsubclN 35556 dihord6apre 36862 dochsscl 36974 mapdordlem2 37243 isnacs3 37590 itgoss 38050 sspwimp 39468 sspwimpVD 39469 nsstr 39587 islptre 40169 gsumlsscl 42489 lincellss 42540 ellcoellss 42549 |
Copyright terms: Public domain | W3C validator |