![]() |
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 3109 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | com12 30 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | sstr2 3109 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | com12 30 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | anim12i 336 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | eqss 3117 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | dfbi2 386 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 5, 6, 7 | 3imtr4i 200 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-11 1485 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-in 3082 df-ss 3089 |
This theorem is referenced by: sseq12 3127 sseq2i 3129 sseq2d 3132 sseqtrid 3152 nssne1 3160 sseq0 3409 un00 3414 pweq 3518 ssintab 3796 ssintub 3797 intmin 3799 treq 4040 ssexg 4075 exmidundif 4137 frforeq3 4277 frirrg 4280 iunpw 4409 ordtri2orexmid 4446 ontr2exmid 4448 onsucsssucexmid 4450 ordtri2or2exmid 4494 fununi 5199 funcnvuni 5200 feq3 5265 ssimaexg 5491 nnawordex 6432 ereq1 6444 xpider 6508 domeng 6654 ssfiexmid 6778 fisseneq 6828 sbthlemi4 6856 sbthlemi5 6857 acfun 7080 ccfunen 7096 basis2 12254 eltg2 12261 clsval 12319 ntrcls0 12339 isnei 12352 neiint 12353 neipsm 12362 opnneissb 12363 opnssneib 12364 innei 12371 icnpimaex 12419 cnptoprest2 12448 neitx 12476 txcnp 12479 blssps 12635 blss 12636 metss 12702 metrest 12714 metcnp3 12719 bdssexg 13273 bj-nntrans 13320 bj-omtrans 13325 |
Copyright terms: Public domain | W3C validator |