![]() |
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 1498 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | dfcleq 2183 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | dfss2 3159 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | dfss2 3159 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | anbi12i 460 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2, 5 | 3bitr4i 212 |
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: eqssi 3186 eqssd 3187 sseq1 3193 sseq2 3194 eqimss 3224 ssrabeq 3257 uneqin 3401 ss0b 3477 vss 3485 sssnm 3769 unidif 3856 ssunieq 3857 iuneq1 3914 iuneq2 3917 iunxdif2 3950 ssext 4236 pweqb 4238 eqopab2b 4294 pwunim 4301 soeq2 4331 iunpw 4495 ordunisuc2r 4528 tfi 4596 eqrel 4730 eqrelrel 4742 coeq1 4799 coeq2 4800 cnveq 4816 dmeq 4842 relssres 4960 xp11m 5082 xpcanm 5083 xpcan2m 5084 ssrnres 5086 fnres 5347 eqfnfv3 5631 fneqeql2 5641 fconst4m 5752 f1imaeq 5792 eqoprab2b 5949 fo1stresm 6180 fo2ndresm 6181 nnacan 6531 nnmcan 6538 ixpeq2 6730 sbthlemi3 6976 isprm2 12135 lssle0 13649 bastop1 13980 epttop 13987 opnneiid 14061 cnntr 14122 metequiv 14392 bj-sseq 14941 bdeq0 15016 bdvsn 15023 bdop 15024 bdeqsuc 15030 bj-om 15086 |
Copyright terms: Public domain | W3C validator |