| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. |
| Ref | Expression |
|---|---|
| elsn |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-sn 3242 |
. 2
| |
| 2 | 1 | abeq2i 2250 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: dfpr2 3252 rexsng 3265 ralsng 3276 disjsn 3280 snprc 3282 euabsn 3285 snss 3317 difprsn 3321 pwpw0 3326 eqsn 3332 snsspw 3337 pwsnALT 3362 hbeqel 3384 uni0b 3389 uni0c 3390 iinxsng 3495 iunxsn 3497 rext 3666 exss 3679 frirr 3789 trsuc2 3896 suceloni 4037 fconstopab 4166 dmsnop 4472 iunfopab 4639 fv2 4761 nfunsn 4792 dffv2 4820 fvopabn 4835 fsn 4899 fopabap 4909 fconstfv 4917 fvclss 4924 opabex3 4933 fparlem3 5206 fparlem4 5207 dfec2 5482 snec 5516 ixp0x 5579 xpsnen 5658 pw2en 5671 ac6sfilem3 5674 fimax 5846 indexfi 5878 elirrv 5933 sucprcreg 5935 ranksn 6036 aceq5lem1 6189 aceq5lem2 6190 aceq5lem4 6192 fodomnumlem 6208 onacda 6259 axdc4lem 6310 axcclem 6312 elreal 6768 xrsupexmnf 7623 xrinfmexpnf 7624 snunioolem 7929 fzsuc 8041 fzsn 8047 fzpr 8048 fseq1p1m1lem1 8062 infxpidmlem8OLD 9222 divalgmod 9303 1nprm 9366 sn0top 9768 cctop 9773 sncld 9930 grpsn 10209 ablsn 10302 gapmlem 10330 ringsn 10359 oefil2 11113 elfilmap 11150 zrdivrng 11256 hsn0elch 11587 h1deoi 11939 bnj112 13239 bnj141 13253 bnj145 13257 bnj158 13263 bnj521 13295 ghomsn 14368 dffr5 14463 wfrlem14 14623 wfrlem15 14624 elsingles 14775 dfiota3 14777 fates 14992 restidsing 15101 cbicplem 15247 iscst4 15261 prsubrtr 15497 sbtpsines 15667 idtrgrp 15756 invtrgrp 15757 ccid 16187 cptclsscpt 16256 alexsublem2 16262 alexsublem3 16263 alexsublem4 16264 locfincomp 16338 ist1-2 16366 ist1-3 16367 isufil2 16389 filssufillem 16394 filssufil 16395 ufileulem 16396 ufileu 16397 filcon 16404 flimcls 16412 cnpfillim 16413 opabex3OLD 16525 fimaxOLD 16570 indexfiOLD 16579 fzfi 16610 heiborlem18 16796 pi1fval 16916 0idl 16997 smprngpr 17024 isdmn3 17046 snssiALTVD 17484 snssiALT 17485 pointpsub 18183 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 1593 ax-12 1598 ax-17 1605 ax-4 1608 ax-5o 1610 ax-6o 1613 ax-9o 1763 ax-ext 2123 |
| This theorem depends on definitions: df-bi 220 df-an 339 df-ex 1616 df-sb 1816 df-clab 2129 df-cleq 2134 df-clel 2137 df-sn 3242 |