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 1480 | . 2 | |
2 | dfcleq 2164 | . 2 | |
3 | dfss2 3136 | . . 3 | |
4 | dfss2 3136 | . . 3 | |
5 | 3, 4 | anbi12i 457 | . 2 |
6 | 1, 2, 5 | 3bitr4i 211 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wal 1346 wceq 1348 wcel 2141 wss 3121 |
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 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-in 3127 df-ss 3134 |
This theorem is referenced by: eqssi 3163 eqssd 3164 sseq1 3170 sseq2 3171 eqimss 3201 ssrabeq 3234 uneqin 3378 ss0b 3453 vss 3461 sssnm 3739 unidif 3826 ssunieq 3827 iuneq1 3884 iuneq2 3887 iunxdif2 3919 ssext 4204 pweqb 4206 eqopab2b 4262 pwunim 4269 soeq2 4299 iunpw 4463 ordunisuc2r 4496 tfi 4564 eqrel 4698 eqrelrel 4710 coeq1 4766 coeq2 4767 cnveq 4783 dmeq 4809 relssres 4927 xp11m 5047 xpcanm 5048 xpcan2m 5049 ssrnres 5051 fnres 5312 eqfnfv3 5593 fneqeql2 5602 fconst4m 5713 f1imaeq 5751 eqoprab2b 5908 fo1stresm 6137 fo2ndresm 6138 nnacan 6488 nnmcan 6495 ixpeq2 6686 sbthlemi3 6932 isprm2 12058 bastop1 12836 epttop 12843 opnneiid 12917 cnntr 12978 metequiv 13248 bj-sseq 13786 bdeq0 13862 bdvsn 13869 bdop 13870 bdeqsuc 13876 bj-om 13932 |
Copyright terms: Public domain | W3C validator |