![]() |
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 3177 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | com12 30 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | sstr2 3177 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | com12 30 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | anim12i 338 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | eqss 3185 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | dfbi2 388 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 5, 6, 7 | 3imtr4i 201 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-in 3150 df-ss 3157 |
This theorem is referenced by: sseq12 3195 sseq2i 3197 sseq2d 3200 sseqtrid 3220 nssne1 3228 sseq0 3479 un00 3484 pweq 3593 ssintab 3876 ssintub 3877 intmin 3879 treq 4122 ssexg 4157 exmidundif 4224 frforeq3 4365 frirrg 4368 iunpw 4498 ordtri2orexmid 4540 ontr2exmid 4542 onsucsssucexmid 4544 ordtri2or2exmid 4588 ontri2orexmidim 4589 iotaexab 5214 fununi 5303 funcnvuni 5304 feq3 5369 ssimaexg 5599 nnawordex 6555 ereq1 6567 xpider 6633 domeng 6779 ssfiexmid 6905 fisseneq 6961 sbthlemi4 6990 sbthlemi5 6991 acfun 7237 onntri45 7271 ccfunen 7294 fprodssdc 11633 lspf 13722 lspval 13723 basis2 14025 eltg2 14030 clsval 14088 ntrcls0 14108 isnei 14121 neiint 14122 neipsm 14131 opnneissb 14132 opnssneib 14133 innei 14140 icnpimaex 14188 cnptoprest2 14217 neitx 14245 txcnp 14248 blssps 14404 blss 14405 metss 14471 metrest 14483 metcnp3 14488 bdssexg 15134 bj-nntrans 15181 bj-omtrans 15186 |
Copyright terms: Public domain | W3C validator |