![]() |
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 1373 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | dfcleq 2031 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | dfss2 2928 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | dfss2 2928 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | anbi12i 433 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2, 5 | 3bitr4i 201 |
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 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-11 1394 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-sb 1643 df-clab 2024 df-cleq 2030 df-clel 2033 df-in 2918 df-ss 2925 |
This theorem is referenced by: eqssi 2955 eqssd 2956 sseq1 2960 sseq2 2961 eqimss 2991 ssrabeq 3020 dfpss3 3024 uneqin 3182 ss0b 3250 vss 3258 sssnm 3516 unidif 3603 ssunieq 3604 iuneq1 3661 iuneq2 3664 iunxdif2 3696 ssext 3948 pweqb 3950 eqopab2b 4007 pwunim 4014 soeq2 4044 iunpw 4177 ordunisuc2r 4205 tfi 4248 eqrel 4372 eqrelrel 4384 coeq1 4436 coeq2 4437 cnveq 4452 dmeq 4478 relssres 4591 xp11m 4702 xpcanm 4703 xpcan2m 4704 ssrnres 4706 fnres 4958 eqfnfv3 5210 fneqeql2 5219 fconst4m 5324 f1imaeq 5357 eqoprab2b 5505 fo1stresm 5730 fo2ndresm 5731 nnacan 6021 nnmcan 6028 bj-sseq 9266 bdeq0 9322 bdvsn 9329 bdop 9330 bdeqsuc 9336 bj-om 9396 |
Copyright terms: Public domain | W3C validator |