![]() |
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 3162 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | com12 30 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | sstr2 3162 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | com12 30 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | anim12i 338 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | eqss 3170 |
. 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 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 |
This theorem is referenced by: sseq12 3180 sseq2i 3182 sseq2d 3185 sseqtrid 3205 nssne1 3213 sseq0 3464 un00 3469 pweq 3577 ssintab 3859 ssintub 3860 intmin 3862 treq 4104 ssexg 4139 exmidundif 4203 frforeq3 4344 frirrg 4347 iunpw 4477 ordtri2orexmid 4519 ontr2exmid 4521 onsucsssucexmid 4523 ordtri2or2exmid 4567 ontri2orexmidim 4568 fununi 5280 funcnvuni 5281 feq3 5346 ssimaexg 5574 nnawordex 6524 ereq1 6536 xpider 6600 domeng 6746 ssfiexmid 6870 fisseneq 6925 sbthlemi4 6953 sbthlemi5 6954 acfun 7200 onntri45 7234 ccfunen 7254 fprodssdc 11582 basis2 13213 eltg2 13220 clsval 13278 ntrcls0 13298 isnei 13311 neiint 13312 neipsm 13321 opnneissb 13322 opnssneib 13323 innei 13330 icnpimaex 13378 cnptoprest2 13407 neitx 13435 txcnp 13438 blssps 13594 blss 13595 metss 13661 metrest 13673 metcnp3 13678 bdssexg 14312 bj-nntrans 14359 bj-omtrans 14364 |
Copyright terms: Public domain | W3C validator |