![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sstr2 | Structured version Visualization version GIF version |
Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Ref | Expression |
---|---|
sstr2 | ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3848 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | imim1d 82 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) |
3 | 2 | alimdv 1875 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) |
4 | dfss2 3842 | . 2 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) | |
5 | dfss2 3842 | . 2 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) | |
6 | 3, 4, 5 | 3imtr4g 288 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1505 ∈ wcel 2048 ⊆ wss 3825 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-clab 2754 df-cleq 2765 df-clel 2840 df-in 3832 df-ss 3839 |
This theorem is referenced by: sstr 3862 sstri 3863 sseq1 3878 sseq2 3879 ssun3 4035 ssun4 4036 ssinss1 4096 triun 5037 trintss 5042 sspwb 5191 exss 5205 frss 5367 relss 5499 funss 6201 funimass2 6264 fss 6351 suceloni 7338 limsssuc 7375 oaordi 7965 oeworde 8012 nnaordi 8037 sbthlem2 8416 sbthlem3 8417 sbthlem6 8420 domunfican 8578 fiint 8582 fiss 8675 dffi3 8682 inf3lem1 8877 trcl 8956 tcss 8972 ac10ct 9246 ackbij2lem4 9454 cfslb 9478 cfslbn 9479 cfcoflem 9484 coftr 9485 fin23lem15 9546 fin23lem20 9549 fin23lem36 9560 isf32lem1 9565 axdc3lem2 9663 ttukeylem2 9722 wunex2 9950 tskcard 9993 clsslem 14195 mrcss 16735 isacs2 16772 lubss 17579 frmdss2 17859 lsmlub 18539 lsslss 19445 lspss 19468 aspss 19816 mplcoe1 19949 mplcoe5 19952 ocv2ss 20509 ocvsscon 20511 lindsss 20660 lsslinds 20667 mdetunilem9 20923 tgss 21270 tgcl 21271 tgss3 21288 clsss 21356 ntrss 21357 neiss 21411 ssnei2 21418 opnnei 21422 cnpnei 21566 cnpco 21569 cncls 21576 cnprest 21591 hauscmp 21709 1stcfb 21747 1stcelcls 21763 reftr 21816 txcnpi 21910 txcnp 21922 txtube 21942 qtoptop2 22001 fgcl 22180 filssufilg 22213 ufileu 22221 uffix 22223 elfm2 22250 fmfnfmlem1 22256 fmco 22263 fbflim2 22279 flffbas 22297 flftg 22298 cnpflf2 22302 alexsubALTlem4 22352 neibl 22804 metcnp3 22843 xlebnum 23262 lebnumii 23263 caubl 23604 caublcls 23605 bcthlem2 23621 bcthlem5 23624 ovolsslem 23778 volsuplem 23849 dyadmbllem 23893 ellimc3 24170 limciun 24185 cpnord 24225 ubthlem1 28415 occon3 28845 chsupval 28883 chsupcl 28888 chsupss 28890 spanss 28896 chsupval2 28958 stlei 29788 dmdbr5 29856 mdsl0 29858 chrelat2i 29913 chirredlem1 29938 mdsymlem5 29955 mdsymlem6 29956 gsumle 30478 gsumvsca1 30481 gsumvsca2 30482 omsmon 31158 cvmliftlem15 32090 ss2mcls 32275 mclsax 32276 clsint2 33138 fgmin 33179 filnetlem4 33190 limsucncmpi 33253 bj-restpw 33828 bj-0int 33838 rdgssun 34036 ptrecube 34281 heiborlem1 34479 heiborlem8 34486 refrelsredund4 35260 refrelredund4 35263 funALTVss 35325 pclssN 36423 dochexmidlem7 37995 incssnn0 38648 islssfg2 39012 hbtlem6 39070 hess 39434 psshepw 39442 clsf2 39784 mnuunid 39933 sspwimpcf 40617 sspwimpcfVD 40618 dvmptfprod 41606 sprsymrelfo 42967 elbigo2 43920 setrec1lem2 44098 setrec1lem4 44100 |
Copyright terms: Public domain | W3C validator |