![]() |
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 2730 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) | |
2 | df-sn 4634 | . 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵} | |
3 | 1, 2 | elab2g 3668 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∈ wcel 2099 {csn 4633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-sn 4634 |
This theorem is referenced by: elsn 4648 elsni 4650 snidg 4667 eltpg 4694 eldifsn 4795 sneqrg 4846 elsucg 6444 ltxr 13149 elfzp12 13634 fprodn0f 15993 lcmfunsnlem2 16641 ramcl 17031 initoeu2lem1 18036 pmtrdifellem4 19477 psdmul 22160 logbmpt 26816 2lgslem2 27424 elunsn 32438 xrge0tsmsbi 32927 rprmnz 33395 dimkerim 33522 elzrhunit 33794 esumrnmpt2 33901 plymulx 34394 bj-projval 36703 bj-elsn12g 36767 bj-elsnb 36768 bj-snmoore 36820 bj-elsn0 36862 eldmressnALTV 37970 brressn 38139 zndvdchrrhm 41669 aks4d1p6 41780 aks6d1c2lem4 41825 sticksstones11 41854 aks6d1c6lem2 41869 aks6d1c7lem1 41878 rhmqusspan 41883 metakunt20 41910 reclimc 45274 itgsincmulx 45595 dirkercncflem2 45725 dirkercncflem4 45727 fourierdlem53 45780 fourierdlem58 45785 fourierdlem60 45787 fourierdlem61 45788 fourierdlem62 45789 fourierdlem76 45803 fourierdlem101 45828 elaa2 45855 etransc 45904 qndenserrnbl 45916 sge0tsms 46001 el1fzopredsuc 46938 clnbupgrel 47405 mndtcob 48409 |
Copyright terms: Public domain | W3C validator |