![]() |
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 3032 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | com12 30 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | sstr2 3032 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | com12 30 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | anim12i 331 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | eqss 3040 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | dfbi2 380 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 5, 6, 7 | 3imtr4i 199 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-11 1442 ax-4 1445 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-i5r 1473 ax-ext 2070 |
This theorem depends on definitions: df-bi 115 df-nf 1395 df-sb 1693 df-clab 2075 df-cleq 2081 df-clel 2084 df-in 3005 df-ss 3012 |
This theorem is referenced by: sseq12 3049 sseq2i 3051 sseq2d 3054 syl5sseq 3074 nssne1 3082 sseq0 3324 un00 3329 pweq 3432 ssintab 3705 ssintub 3706 intmin 3708 treq 3942 ssexg 3978 exmidundif 4035 frforeq3 4174 frirrg 4177 iunpw 4302 ordtri2orexmid 4339 ontr2exmid 4341 onsucsssucexmid 4343 ordtri2or2exmid 4387 fununi 5082 funcnvuni 5083 feq3 5147 ssimaexg 5366 nnawordex 6287 ereq1 6299 xpiderm 6363 domeng 6469 ssfiexmid 6592 fisseneq 6642 sbthlemi4 6669 sbthlemi5 6670 bdssexg 11795 bj-nntrans 11846 bj-omtrans 11851 |
Copyright terms: Public domain | W3C validator |