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 4573 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1528 ∈ wcel 2105 Vcvv 3495 {csn 4559 |
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 2793 |
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 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-sn 4560 |
This theorem is referenced by: velsn 4575 opthwiener 5396 opthprc 5610 dmsnn0 6058 dmsnopg 6064 cnvcnvsn 6070 snsn0non 6303 funconstss 6819 fniniseg 6823 fniniseg2 6825 fsn 6890 fconstfv 6967 eusvobj2 7138 fnse 7818 wfrlem14 7959 fisn 8880 axdc3lem4 9864 axdc4lem 9866 axcclem 9868 opelreal 10541 seqid3 13404 seqz 13408 1exp 13448 hashf1lem2 13804 fprodn0f 15335 imasaddfnlem 16791 initoid 17255 termoid 17256 0subm 17972 grpinvfval 18082 0subg 18244 0nsg 18261 sylow2alem2 18674 gsumval3 18958 gsumzaddlem 18972 kerf1ghm 19428 kerf1hrmOLD 19429 lsssn0 19650 r0cld 22276 alexsubALTlem2 22586 tgphaus 22654 isusp 22799 i1f1lem 24219 ig1pcl 24698 plyco0 24711 plyeq0lem 24729 plycj 24796 wilthlem2 25574 dchrfi 25759 snstriedgval 26751 incistruhgr 26792 1loopgrnb0 27212 umgr2v2enb1 27236 usgr2pthlem 27472 hsn0elch 28953 h1de2ctlem 29260 atomli 30087 brsnop 30356 1stpreimas 30368 gsummpt2d 30615 kerunit 30824 qqhval2lem 31122 qqhf 31127 qqhre 31161 esum2dlem 31251 eulerpartlemb 31526 bnj149 32047 subfacp1lem6 32330 ellimits 33269 bj-0nel1 34163 bj-isrvec 34464 poimirlem18 34792 poimirlem21 34795 poimirlem22 34796 poimirlem31 34805 poimirlem32 34806 itg2addnclem2 34826 ftc1anclem3 34851 0idl 35186 keridl 35193 smprngopr 35213 isdmn3 35235 ellkr 36107 diblss 38188 dihmeetlem4preN 38324 dihmeetlem13N 38337 0prjspnrel 39149 pw2f1ocnv 39514 fvnonrel 39837 snhesn 40012 unirnmapsn 41357 sge0fodjrnlem 42579 smndex1mgm 43977 smndex1n0mnd 43982 lindslinindsimp1 44410 |
Copyright terms: Public domain | W3C validator |