![]() |
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 3902 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | |
2 | 1 | imp 407 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ⊆ wss 3865 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-in 3872 df-ss 3880 |
This theorem is referenced by: sstrd 3905 sylan9ss 3908 ssdifss 4039 uneqin 4181 ssrnres 5918 relrelss 6006 fco 6406 fssres 6419 ssimaex 6622 dff3 6736 tpostpos2 7771 smores 7848 om00 8058 omeulem2 8066 pmss12g 8290 unblem1 8623 unblem2 8624 unblem3 8625 unblem4 8626 isfinite2 8629 cantnfval2 8985 cantnfle 8987 rankxplim3 9163 alephinit 9374 dfac12lem2 9423 ackbij1lem11 9505 cfeq0 9531 cfsuc 9532 cff1 9533 cflim2 9538 cfss 9540 cfslb2n 9543 cofsmo 9544 cfsmolem 9545 fin23lem34 9621 fin1a2lem13 9687 axdc3lem2 9726 axdclem 9794 pwcfsdom 9858 wunfi 9996 tskxpss 10047 tskcard 10056 suprzcl 11916 uzwo 12164 uzwo2 12165 infssuzle 12184 infssuzcl 12185 supxrbnd 12575 supxrgtmnf 12576 supxrre1 12577 supxrre2 12578 supxrss 12579 infxrss 12586 iccsupr 12684 hashf1lem2 13666 trclun 14212 fsum2d 14963 fsumabs 14993 fsumrlim 15003 fsumo1 15004 fprod2d 15172 rpnnen2lem4 15407 rpnnen2lem7 15410 ramub2 16183 ressinbas 16393 ressress 16395 submre 16709 mrcss 16720 mreacs 16762 drsdirfi 17381 clatglbss 17570 ipopos 17603 cntz2ss 18208 ablfac1eulem 18915 subrgint 19251 tgval 21251 mretopd 21388 ssnei 21406 opnneiss 21414 restdis 21474 restcls 21477 restntr 21478 tgcnp 21549 fbssfi 22133 fgss2 22170 fgcl 22174 supfil 22191 alexsubALTlem3 22345 alexsubALTlem4 22346 cnextcn 22363 ustex3sym 22513 trust 22525 restutop 22533 utop2nei 22546 cfiluweak 22591 blssexps 22723 blssex 22724 mopni3 22791 metss 22805 metcnp3 22837 metust 22855 cfilucfil 22856 psmetutop 22864 tgioo 23091 xrsmopn 23107 fsumcn 23165 cncfmptid 23207 iscmet3lem2 23582 caussi 23587 ovolsslem 23772 ovolsscl 23774 ovolssnul 23775 opnmblALT 23891 itgfsum 24114 limcresi 24170 dvmptfsum 24259 plyss 24476 nbuhgr 26812 chsupunss 28808 shsupunss 28810 spanss 28812 shslubi 28849 shlub 28878 mdsl1i 29785 mdsl2i 29786 cvmdi 29788 mdslmd1lem1 29789 mdslmd1lem2 29790 mdslmd2i 29794 mdslmd4i 29797 atomli 29846 atcvatlem 29849 chirredlem2 29855 chirredi 29858 mdsymlem5 29871 xrge0infss 30168 tpr2rico 30768 sigainb 31008 dya2icoseg2 31149 omssubadd 31171 eulerpartlemn 31252 ballotlem2 31359 cvmlift2lem12 32171 opnbnd 33284 fneint 33307 bj-intss 34011 dissneqlem 34173 inunissunidif 34208 pibt2 34250 fin2so 34431 matunitlindflem1 34440 mblfinlem4 34484 ismblfin 34485 filbcmb 34568 heiborlem10 34651 igenmin 34895 lssatle 35703 paddss1 36505 paddss2 36506 paddss12 36507 paddssw2 36532 pclssN 36582 pclfinN 36588 polsubN 36595 2polvalN 36602 2polssN 36603 3polN 36604 2pmaplubN 36614 pnonsingN 36621 polsubclN 36640 dihord6apre 37944 dochsscl 38056 mapdordlem2 38325 isnacs3 38813 itgoss 39269 sspwimp 40812 sspwimpVD 40813 nsstr 40921 islptre 41463 gsumlsscl 43933 lincellss 43983 ellcoellss 43992 |
Copyright terms: Public domain | W3C validator |