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 3575 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | |
2 | 1 | imp 444 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ⊆ wss 3540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-in 3547 df-ss 3554 |
This theorem is referenced by: sstrd 3578 sylan9ss 3581 ssdifss 3703 uneqin 3837 ssrnres 5491 relrelss 5576 fco 5971 fssres 5983 ssimaex 6173 dff3 6280 tpostpos2 7260 smores 7336 om00 7542 omeulem2 7550 pmss12g 7770 unblem1 8097 unblem2 8098 unblem3 8099 unblem4 8100 isfinite2 8103 cantnfval2 8449 cantnfle 8451 rankxplim3 8627 alephinit 8801 dfac12lem2 8849 ackbij1lem11 8935 cfeq0 8961 cfsuc 8962 cff1 8963 cflim2 8968 cfss 8970 cfslb2n 8973 cofsmo 8974 cfsmolem 8975 fin23lem34 9051 fin1a2lem13 9117 axdc3lem2 9156 axdclem 9224 pwcfsdom 9284 wunfi 9422 tskxpss 9473 tskcard 9482 suprzcl 11333 uzwo 11627 uzwo2 11628 infssuzle 11647 infssuzcl 11648 supxrbnd 12030 supxrgtmnf 12031 supxrre1 12032 supxrre2 12033 supxrss 12034 infxrss 12040 iccsupr 12137 hashf1lem2 13097 trclun 13603 fsum2d 14344 fsumabs 14374 fsumrlim 14384 fsumo1 14385 fprod2d 14550 rpnnen2lem4 14785 rpnnen2lem7 14788 ramub2 15556 ressinbas 15763 ressress 15765 submre 16088 mrcss 16099 mreacs 16142 drsdirfi 16761 clatglbss 16950 ipopos 16983 cntz2ss 17588 ablfac1eulem 18294 subrgint 18625 tgval 20570 mretopd 20706 ssnei 20724 opnneiss 20732 restdis 20792 restcls 20795 restntr 20796 tgcnp 20867 fbssfi 21451 fgss2 21488 fgcl 21492 supfil 21509 alexsubALTlem3 21663 alexsubALTlem4 21664 cnextcn 21681 ustex3sym 21831 trust 21843 restutop 21851 utop2nei 21864 cfiluweak 21909 blssexps 22041 blssex 22042 mopni3 22109 metss 22123 metcnp3 22155 metust 22173 cfilucfil 22174 psmetutop 22182 tgioo 22407 xrsmopn 22423 fsumcn 22481 cncfmptid 22523 iscmet3lem2 22898 caussi 22903 ovolsslem 23059 ovolsscl 23061 ovolssnul 23062 opnmblALT 23177 itgfsum 23399 limcresi 23455 dvmptfsum 23542 plyss 23759 chsupunss 27587 shsupunss 27589 spanss 27591 shslubi 27628 shlub 27657 mdsl1i 28564 mdsl2i 28565 cvmdi 28567 mdslmd1lem1 28568 mdslmd1lem2 28569 mdslmd2i 28573 mdslmd4i 28576 atomli 28625 atcvatlem 28628 chirredlem2 28634 chirredi 28637 mdsymlem5 28650 xrge0infss 28915 tpr2rico 29286 sigainb 29526 dya2icoseg2 29667 omssubadd 29689 eulerpartlemn 29770 ballotlem2 29877 cvmlift2lem12 30550 opnbnd 31490 fneint 31513 dissneqlem 32363 fin2so 32566 matunitlindflem1 32575 mblfinlem4 32619 ismblfin 32620 filbcmb 32705 heiborlem10 32789 igenmin 33033 lssatle 33320 paddss1 34121 paddss2 34122 paddss12 34123 paddssw2 34148 pclssN 34198 pclfinN 34204 polsubN 34211 2polvalN 34218 2polssN 34219 3polN 34220 2pmaplubN 34230 pnonsingN 34237 polsubclN 34256 dihord6apre 35563 dochsscl 35675 mapdordlem2 35944 isnacs3 36291 itgoss 36752 sspwimp 38176 sspwimpVD 38177 nsstr 38301 islptre 38686 nbuhgr 40565 gsumlsscl 41958 lincellss 42009 ellcoellss 42018 |
Copyright terms: Public domain | W3C validator |