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 2822 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) | |
2 | df-sn 4558 | . 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵} | |
3 | 1, 2 | elab2g 3665 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 {csn 4557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-sn 4558 |
This theorem is referenced by: elsn 4572 elsni 4574 snidg 4589 eltpg 4615 eldifsn 4711 eldifsnneqOLD 4716 sneqrg 4762 elsucg 6251 ltxr 12498 elfzp12 12974 fprodn0f 15333 lcmfunsnlem2 15972 ramcl 16353 initoeu2lem1 17262 pmtrdifellem4 18536 logbmpt 25293 2lgslem2 25898 elunsn 30200 xrge0tsmsbi 30620 dimkerim 30922 elzrhunit 31119 esumrnmpt2 31226 plymulx 31717 bj-projval 34205 bj-elsn12g 34247 bj-elsnb 34248 bj-snmoore 34299 bj-elsn0 34339 reclimc 41810 itgsincmulx 42135 dirkercncflem2 42266 dirkercncflem4 42268 fourierdlem53 42321 fourierdlem58 42326 fourierdlem60 42328 fourierdlem61 42329 fourierdlem62 42330 fourierdlem76 42344 fourierdlem101 42369 elaa2 42396 etransc 42445 qndenserrnbl 42457 sge0tsms 42539 el1fzopredsuc 43402 |
Copyright terms: Public domain | W3C validator |