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 1463 | . 2 | |
2 | dfcleq 2133 | . 2 | |
3 | dfss2 3086 | . . 3 | |
4 | dfss2 3086 | . . 3 | |
5 | 3, 4 | anbi12i 455 | . 2 |
6 | 1, 2, 5 | 3bitr4i 211 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wal 1329 wceq 1331 wcel 1480 wss 3071 |
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 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-in 3077 df-ss 3084 |
This theorem is referenced by: eqssi 3113 eqssd 3114 sseq1 3120 sseq2 3121 eqimss 3151 ssrabeq 3183 uneqin 3327 ss0b 3402 vss 3410 sssnm 3681 unidif 3768 ssunieq 3769 iuneq1 3826 iuneq2 3829 iunxdif2 3861 ssext 4143 pweqb 4145 eqopab2b 4201 pwunim 4208 soeq2 4238 iunpw 4401 ordunisuc2r 4430 tfi 4496 eqrel 4628 eqrelrel 4640 coeq1 4696 coeq2 4697 cnveq 4713 dmeq 4739 relssres 4857 xp11m 4977 xpcanm 4978 xpcan2m 4979 ssrnres 4981 fnres 5239 eqfnfv3 5520 fneqeql2 5529 fconst4m 5640 f1imaeq 5676 eqoprab2b 5829 fo1stresm 6059 fo2ndresm 6060 nnacan 6408 nnmcan 6415 ixpeq2 6606 sbthlemi3 6847 isprm2 11798 bastop1 12252 epttop 12259 opnneiid 12333 cnntr 12394 metequiv 12664 bj-sseq 12999 bdeq0 13065 bdvsn 13072 bdop 13073 bdeqsuc 13079 bj-om 13135 |
Copyright terms: Public domain | W3C validator |