![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elsncg | Structured version Visualization version Unicode version |
Description: There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15 (generalized). (Contributed by NM, 13-Sep-1995.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Ref | Expression |
---|---|
elsncg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2475 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-sn 3960 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | elab2g 3175 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-v 3033 df-sn 3960 |
This theorem is referenced by: elsnc 3984 elsni 3985 snidg 3986 nelsn 3992 eltpg 4005 eldifsn 4088 elsucg 5497 ltxr 11438 elfzp12 11899 fprodn0f 14122 lcmfunsnlem2 14692 ramcl 15066 initoeu2lem1 15987 pmtrdifellem4 17198 logbmpt 23804 nbcusgra 25270 frgrancvvdeqlem1 25837 xrge0tsmsbi 28623 elzrhunit 28857 elzdif0 28858 esumrnmpt2 28963 plymulx 29509 bj-projval 31660 unirnmapsn 37567 reclimc 37831 itgsincmulx 37948 dirkercncflem2 38078 dirkercncflem4 38080 fourierdlem53 38135 fourierdlem58 38140 fourierdlem60 38142 fourierdlem61 38143 fourierdlem62 38144 fourierdlem76 38158 fourierdlem101 38183 elaa2 38211 etransc 38261 qndenserrnbl 38276 sge0tsms 38336 sge0fodjrnlem 38372 el1fzopredsuc 38867 |
Copyright terms: Public domain | W3C validator |