Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sstr2 | Unicode version |
Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Ref | Expression |
---|---|
sstr2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3131 | . . . 4 | |
2 | 1 | imim1d 75 | . . 3 |
3 | 2 | alimdv 1866 | . 2 |
4 | dfss2 3126 | . 2 | |
5 | dfss2 3126 | . 2 | |
6 | 3, 4, 5 | 3imtr4g 204 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1340 wcel 2135 wss 3111 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3117 df-ss 3124 |
This theorem is referenced by: sstr 3145 sstri 3146 sseq1 3160 sseq2 3161 ssun3 3282 ssun4 3283 ssinss1 3346 ssdisj 3460 triun 4087 trintssm 4090 sspwb 4188 exss 4199 relss 4685 funss 5201 funimass2 5260 fss 5343 fiintim 6885 sbthlem2 6914 sbthlemi3 6915 sbthlemi6 6918 tgss 12604 tgcl 12605 tgss3 12619 clsss 12659 neiss 12691 ssnei2 12698 cnpnei 12760 cnptopco 12763 cnptoprest 12780 txcnp 12812 neibl 13032 metcnp3 13052 bj-nntrans 13668 |
Copyright terms: Public domain | W3C validator |