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 2952 | . . . 4 | |
2 | 1 | com12 27 | . . 3 |
3 | sstr2 2952 | . . . 4 | |
4 | 3 | com12 27 | . . 3 |
5 | 2, 4 | anim12i 321 | . 2 |
6 | eqss 2960 | . 2 | |
7 | dfbi2 368 | . 2 | |
8 | 5, 6, 7 | 3imtr4i 190 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wb 98 wceq 1243 wss 2917 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-11 1397 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-in 2924 df-ss 2931 |
This theorem is referenced by: sseq12 2968 sseq2i 2970 sseq2d 2973 syl5sseq 2993 nssne1 3001 psseq2 3032 sseq0 3258 un00 3263 disjpss 3278 pweq 3362 ssintab 3632 ssintub 3633 intmin 3635 treq 3860 ssexg 3896 frforeq3 4084 frirrg 4087 iunpw 4211 ordtri2orexmid 4248 ontr2exmid 4250 onsucsssucexmid 4252 ordtri2or2exmid 4296 fununi 4967 funcnvuni 4968 feq3 5032 ssimaexg 5235 nnawordex 6101 ereq1 6113 xpiderm 6177 domeng 6233 ssfiexmid 6336 bdssexg 10024 bj-nntrans 10076 bj-omtrans 10081 |
Copyright terms: Public domain | W3C validator |