![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elsnc | Structured version Visualization version Unicode version |
Description: There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
Ref | Expression |
---|---|
elsnc.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
elsnc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsnc.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | elsncg 3991 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-v 3047 df-sn 3969 |
This theorem is referenced by: sneqr 4139 opthwiener 4703 opthprc 4882 dmsnn0 5301 dmsnopg 5307 cnvcnvsn 5313 snsn0non 5541 sniota 5573 funconstss 6000 fniniseg 6003 fniniseg2 6005 fsn 6061 fconstfv 6126 eusvobj2 6283 fnse 6913 wfrlem14 7049 fisn 7941 axdc3lem4 8883 axdc4lem 8885 axcclem 8887 ttukeylem7 8945 opelreal 9554 seqid3 12257 seqz 12261 1exp 12301 hashf1lem2 12619 fprodn0f 14045 imasaddfnlem 15434 initoid 15900 termoid 15901 0subg 16842 0nsg 16862 sylow2alem2 17270 gsumval3 17541 gsumzaddlem 17554 kerf1hrm 17971 lsssn0 18171 r0cld 20753 alexsubALTlem2 21063 tgphaus 21131 isusp 21276 i1f1lem 22647 ig1pcl 23127 ig1pclOLD 23133 plyco0 23146 plyeq0lem 23164 plycj 23231 wilthlem2 23994 dchrfi 24183 hsn0elch 26901 h1de2ctlem 27208 atomli 28035 1stpreimas 28286 gsummpt2d 28544 kerunit 28586 qqhval2lem 28785 qqhf 28790 qqhre 28824 esum2dlem 28913 inelpisys 28976 sitgaddlemb 29181 eulerpartlemb 29201 bnj149 29686 subfacp1lem6 29908 ellimits 30677 bj-0nel1 31546 poimirlem18 31958 poimirlem21 31961 poimirlem22 31962 poimirlem31 31971 poimirlem32 31972 itg2addnclem2 31994 ftc1anclem3 32019 0idl 32258 keridl 32265 smprngopr 32285 isdmn3 32307 ellkr 32655 diblss 34738 dihmeetlem4preN 34874 dihmeetlem13N 34887 pw2f1ocnv 35892 fvnonrel 36203 snhesn 36382 snstriedgval 39138 incistruhgr 39171 uspgrloopnb0 39556 umgr2v2enb1 39563 usgra2pthlem1 39720 lindslinindsimp1 40303 |
Copyright terms: Public domain | W3C validator |