![]() |
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 4330 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1631 ∈ wcel 2145 Vcvv 3351 {csn 4316 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 df-sn 4317 |
This theorem is referenced by: velsn 4332 opthwiener 5107 opthprc 5307 dmsnn0 5741 dmsnopg 5748 cnvcnvsn 5754 snsn0non 5989 funconstss 6478 fniniseg 6481 fniniseg2 6483 fsn 6545 fconstfv 6620 eusvobj2 6786 fnse 7445 wfrlem14 7581 mapdm0 8024 fisn 8489 axdc3lem4 9477 axdc4lem 9479 axcclem 9481 opelreal 10153 seqid3 13052 seqz 13056 1exp 13096 hashf1lem2 13442 fprodn0f 14928 imasaddfnlem 16396 initoid 16862 termoid 16863 0subg 17827 0nsg 17847 sylow2alem2 18240 gsumval3 18515 gsumzaddlem 18528 kerf1hrm 18953 lsssn0 19158 r0cld 21762 alexsubALTlem2 22072 tgphaus 22140 isusp 22285 i1f1lem 23676 ig1pcl 24155 plyco0 24168 plyeq0lem 24186 plycj 24253 wilthlem2 25016 dchrfi 25201 snstriedgval 26151 incistruhgr 26195 1loopgrnb0 26633 umgr2v2enb1 26657 usgr2pthlem 26894 hsn0elch 28445 h1de2ctlem 28754 atomli 29581 1stpreimas 29823 gsummpt2d 30121 kerunit 30163 qqhval2lem 30365 qqhf 30370 qqhre 30404 esum2dlem 30494 eulerpartlemb 30770 bnj149 31283 subfacp1lem6 31505 ellimits 32354 bj-0nel1 33271 poimirlem18 33760 poimirlem21 33763 poimirlem22 33764 poimirlem31 33773 poimirlem32 33774 itg2addnclem2 33794 ftc1anclem3 33819 0idl 34156 keridl 34163 smprngopr 34183 isdmn3 34205 ellkr 34898 diblss 36980 dihmeetlem4preN 37116 dihmeetlem13N 37129 pw2f1ocnv 38130 fvnonrel 38429 snhesn 38606 unirnmapsn 39924 sge0fodjrnlem 41150 lindslinindsimp1 42774 |
Copyright terms: Public domain | W3C validator |