Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sseq2 | Unicode version |
Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.) |
Ref | Expression |
---|---|
sseq2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstr2 3144 | . . . 4 | |
2 | 1 | com12 30 | . . 3 |
3 | sstr2 3144 | . . . 4 | |
4 | 3 | com12 30 | . . 3 |
5 | 2, 4 | anim12i 336 | . 2 |
6 | eqss 3152 | . 2 | |
7 | dfbi2 386 | . 2 | |
8 | 5, 6, 7 | 3imtr4i 200 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wceq 1342 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: sseq12 3162 sseq2i 3164 sseq2d 3167 sseqtrid 3187 nssne1 3195 sseq0 3445 un00 3450 pweq 3556 ssintab 3835 ssintub 3836 intmin 3838 treq 4080 ssexg 4115 exmidundif 4179 frforeq3 4319 frirrg 4322 iunpw 4452 ordtri2orexmid 4494 ontr2exmid 4496 onsucsssucexmid 4498 ordtri2or2exmid 4542 ontri2orexmidim 4543 fununi 5250 funcnvuni 5251 feq3 5316 ssimaexg 5542 nnawordex 6487 ereq1 6499 xpider 6563 domeng 6709 ssfiexmid 6833 fisseneq 6888 sbthlemi4 6916 sbthlemi5 6917 acfun 7154 onntri45 7188 ccfunen 7196 fprodssdc 11517 basis2 12593 eltg2 12600 clsval 12658 ntrcls0 12678 isnei 12691 neiint 12692 neipsm 12701 opnneissb 12702 opnssneib 12703 innei 12710 icnpimaex 12758 cnptoprest2 12787 neitx 12815 txcnp 12818 blssps 12974 blss 12975 metss 13041 metrest 13053 metcnp3 13058 bdssexg 13627 bj-nntrans 13674 bj-omtrans 13679 |
Copyright terms: Public domain | W3C validator |