![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elsn | Structured version Visualization version GIF version |
Description: There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
Ref | Expression |
---|---|
elsn.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
elsn | ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsn.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | elsng 4488 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1522 ∈ wcel 2080 Vcvv 3436 {csn 4474 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-ext 2768 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-sn 4475 |
This theorem is referenced by: velsn 4490 opthwiener 5298 opthprc 5505 dmsnn0 5942 dmsnopg 5948 cnvcnvsn 5954 snsn0non 6187 funconstss 6694 fniniseg 6698 fniniseg2 6700 fsn 6763 fconstfv 6844 eusvobj2 7012 fnse 7683 wfrlem14 7823 fisn 8740 axdc3lem4 9724 axdc4lem 9726 axcclem 9728 opelreal 10401 seqid3 13264 seqz 13268 1exp 13308 hashf1lem2 13662 fprodn0f 15178 imasaddfnlem 16630 initoid 17094 termoid 17095 grpinvfval 17899 0subg 18058 0nsg 18078 sylow2alem2 18473 gsumval3 18748 gsumzaddlem 18761 kerf1ghm 19187 kerf1hrmOLD 19188 lsssn0 19409 r0cld 22030 alexsubALTlem2 22340 tgphaus 22408 isusp 22553 i1f1lem 23973 ig1pcl 24452 plyco0 24465 plyeq0lem 24483 plycj 24550 wilthlem2 25328 dchrfi 25513 snstriedgval 26506 incistruhgr 26547 1loopgrnb0 26967 umgr2v2enb1 26991 usgr2pthlem 27226 hsn0elch 28708 h1de2ctlem 29015 atomli 29842 brsnop 30109 1stpreimas 30121 gsummpt2d 30488 kerunit 30542 qqhval2lem 30831 qqhf 30836 qqhre 30870 esum2dlem 30960 eulerpartlemb 31235 bnj149 31755 subfacp1lem6 32034 ellimits 32974 bj-0nel1 33834 poimirlem18 34454 poimirlem21 34457 poimirlem22 34458 poimirlem31 34467 poimirlem32 34468 itg2addnclem2 34488 ftc1anclem3 34513 0idl 34848 keridl 34855 smprngopr 34875 isdmn3 34897 ellkr 35769 diblss 37850 dihmeetlem4preN 37986 dihmeetlem13N 37999 0prjspnrel 38779 pw2f1ocnv 39132 fvnonrel 39455 snhesn 39630 unirnmapsn 41030 sge0fodjrnlem 42254 lindslinindsimp1 44006 |
Copyright terms: Public domain | W3C validator |