![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqss | Unicode version |
Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqss |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albiim 1431 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | dfcleq 2094 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | dfss2 3036 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | dfss2 3036 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | anbi12i 451 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2, 5 | 3bitr4i 211 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-11 1452 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-in 3027 df-ss 3034 |
This theorem is referenced by: eqssi 3063 eqssd 3064 sseq1 3070 sseq2 3071 eqimss 3101 ssrabeq 3130 uneqin 3274 ss0b 3349 vss 3357 sssnm 3628 unidif 3715 ssunieq 3716 iuneq1 3773 iuneq2 3776 iunxdif2 3808 ssext 4081 pweqb 4083 eqopab2b 4139 pwunim 4146 soeq2 4176 iunpw 4339 ordunisuc2r 4368 tfi 4434 eqrel 4566 eqrelrel 4578 coeq1 4634 coeq2 4635 cnveq 4651 dmeq 4677 relssres 4793 xp11m 4913 xpcanm 4914 xpcan2m 4915 ssrnres 4917 fnres 5175 eqfnfv3 5452 fneqeql2 5461 fconst4m 5572 f1imaeq 5608 eqoprab2b 5761 fo1stresm 5990 fo2ndresm 5991 nnacan 6338 nnmcan 6345 ixpeq2 6536 sbthlemi3 6775 isprm2 11591 bastop1 12034 epttop 12041 opnneiid 12115 cnntr 12175 metequiv 12423 bj-sseq 12580 bdeq0 12646 bdvsn 12653 bdop 12654 bdeqsuc 12660 bj-om 12720 |
Copyright terms: Public domain | W3C validator |