![]() |
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 2775 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵)) | |
2 | df-sn 4436 | . 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵} | |
3 | 1, 2 | elab2g 3577 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1508 ∈ wcel 2051 {csn 4435 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2743 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-sn 4436 |
This theorem is referenced by: elsn 4450 elsni 4452 snidg 4467 eltpg 4493 eldifsn 4589 eldifsnneqOLD 4594 sneqrg 4640 elsucg 6093 ltxr 12325 elfzp12 12800 fprodn0f 15203 lcmfunsnlem2 15838 ramcl 16219 initoeu2lem1 17144 pmtrdifellem4 18380 logbmpt 25082 2lgslem2 25688 xrge0tsmsbi 30563 dimkerim 30684 elzrhunit 30896 esumrnmpt2 31003 plymulx 31496 bj-projval 33863 bj-snmoore 33953 reclimc 41399 itgsincmulx 41723 dirkercncflem2 41854 dirkercncflem4 41856 fourierdlem53 41909 fourierdlem58 41914 fourierdlem60 41916 fourierdlem61 41917 fourierdlem62 41918 fourierdlem76 41932 fourierdlem101 41957 elaa2 41984 etransc 42033 qndenserrnbl 42045 sge0tsms 42127 el1fzopredsuc 42965 |
Copyright terms: Public domain | W3C validator |