| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elsng | Structured version Visualization version GIF 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 |
|---|---|
| elsng | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqeq1 2741 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) | |
| 2 | df-sn 4627 | . 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵} | |
| 3 | 1, 2 | elab2g 3680 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 {csn 4626 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-sn 4627 |
| This theorem is referenced by: elsn 4641 elsni 4643 snidg 4660 elunsn 4683 eltpg 4686 el7g 4690 eldifsn 4786 sneqrg 4839 elsucg 6452 ltxr 13157 elfzp12 13643 fzdif1 13645 fprodn0f 16027 lcmfunsnlem2 16677 ramcl 17067 initoeu2lem1 18059 pmtrdifellem4 19497 psdmul 22170 logbmpt 26831 2lgslem2 27439 xrge0tsmsbi 33066 rprmnz 33548 dimkerim 33678 elzrhunit 33978 esumrnmpt2 34069 plymulx 34563 bj-projval 36997 bj-elsn12g 37061 bj-elsnb 37062 bj-snmoore 37114 bj-elsn0 37156 eldmressnALTV 38273 brressn 38442 zndvdchrrhm 41972 aks4d1p6 42082 aks6d1c2lem4 42128 sticksstones11 42157 aks6d1c6lem2 42172 aks6d1c7lem1 42181 rhmqusspan 42186 unitscyglem2 42197 metakunt20 42225 reclimc 45668 itgsincmulx 45989 dirkercncflem2 46119 dirkercncflem4 46121 fourierdlem53 46174 fourierdlem58 46179 fourierdlem60 46181 fourierdlem61 46182 fourierdlem62 46183 fourierdlem76 46197 fourierdlem101 46222 elaa2 46249 etransc 46298 qndenserrnbl 46310 sge0tsms 46395 el1fzopredsuc 47337 elclnbgrelnbgr 47812 clnbupgrel 47821 mndtcob 49179 |
| Copyright terms: Public domain | W3C validator |