![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > elsncg | Unicode version |
Description: There is only 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 2461 | . 2 | |
2 | df-sn 4030 | . 2 | |
3 | 1, 2 | elab2g 3248 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 <-> wb 184
= wceq 1395 e. wcel 1818 { csn 4029 |
This theorem is referenced by: elsnc 4053 elsni 4054 snidg 4055 eltpg 4071 eldifsn 4155 elsucg 4950 ltxr 11353 elfzp12 11786 ramcl 14547 pmtrdifellem4 16504 nbcusgra 24463 frgrancvvdeqlem1 25030 xrge0tsmsbi 27776 elzrhunit 27960 elzdif0 27961 plymulx 28505 fprodn0f 31594 reclimc 31659 itgsincmulx 31773 dirkercncflem2 31886 dirkercncflem4 31888 fourierdlem53 31942 fourierdlem58 31947 fourierdlem60 31949 fourierdlem61 31950 fourierdlem62 31951 fourierdlem76 31965 fourierdlem101 31990 elaa2 32017 etransc 32066 initoeu2lem1 32620 bj-projval 34554 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-v 3111 df-sn 4030 |
Copyright terms: Public domain | W3C validator |