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 1474 | . 2 | |
2 | dfcleq 2158 | . 2 | |
3 | dfss2 3126 | . . 3 | |
4 | dfss2 3126 | . . 3 | |
5 | 3, 4 | anbi12i 456 | . 2 |
6 | 1, 2, 5 | 3bitr4i 211 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wal 1340 wceq 1342 wcel 2135 wss 3111 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3117 df-ss 3124 |
This theorem is referenced by: eqssi 3153 eqssd 3154 sseq1 3160 sseq2 3161 eqimss 3191 ssrabeq 3224 uneqin 3368 ss0b 3443 vss 3451 sssnm 3728 unidif 3815 ssunieq 3816 iuneq1 3873 iuneq2 3876 iunxdif2 3908 ssext 4193 pweqb 4195 eqopab2b 4251 pwunim 4258 soeq2 4288 iunpw 4452 ordunisuc2r 4485 tfi 4553 eqrel 4687 eqrelrel 4699 coeq1 4755 coeq2 4756 cnveq 4772 dmeq 4798 relssres 4916 xp11m 5036 xpcanm 5037 xpcan2m 5038 ssrnres 5040 fnres 5298 eqfnfv3 5579 fneqeql2 5588 fconst4m 5699 f1imaeq 5737 eqoprab2b 5891 fo1stresm 6121 fo2ndresm 6122 nnacan 6471 nnmcan 6478 ixpeq2 6669 sbthlemi3 6915 isprm2 12028 bastop1 12624 epttop 12631 opnneiid 12705 cnntr 12766 metequiv 13036 bj-sseq 13508 bdeq0 13584 bdvsn 13591 bdop 13592 bdeqsuc 13598 bj-om 13654 |
Copyright terms: Public domain | W3C validator |