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 4139 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 ∈ wcel 1977 Vcvv 3173 {csn 4125 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-sn 4126 |
This theorem is referenced by: velsn 4141 opthwiener 4901 opthprc 5089 dmsnn0 5518 dmsnopg 5524 cnvcnvsn 5530 snsn0non 5763 funconstss 6243 fniniseg 6246 fniniseg2 6248 fsn 6308 fconstfv 6381 eusvobj2 6542 fnse 7181 wfrlem14 7315 fisn 8216 axdc3lem4 9158 axdc4lem 9160 axcclem 9162 opelreal 9830 seqid3 12707 seqz 12711 1exp 12751 hashf1lem2 13097 fprodn0f 14561 imasaddfnlem 16011 initoid 16478 termoid 16479 0subg 17442 0nsg 17462 sylow2alem2 17856 gsumval3 18131 gsumzaddlem 18144 kerf1hrm 18566 lsssn0 18769 r0cld 21351 alexsubALTlem2 21662 tgphaus 21730 isusp 21875 i1f1lem 23262 ig1pcl 23739 plyco0 23752 plyeq0lem 23770 plycj 23837 wilthlem2 24595 dchrfi 24780 snstriedgval 25713 incistruhgr 25746 hsn0elch 27489 h1de2ctlem 27798 atomli 28625 1stpreimas 28866 gsummpt2d 29112 kerunit 29154 qqhval2lem 29353 qqhf 29358 qqhre 29392 esum2dlem 29481 eulerpartlemb 29757 bnj149 30199 subfacp1lem6 30421 ellimits 31187 bj-0nel1 32133 poimirlem18 32597 poimirlem21 32600 poimirlem22 32601 poimirlem31 32610 poimirlem32 32611 itg2addnclem2 32632 ftc1anclem3 32657 0idl 32994 keridl 33001 smprngopr 33021 isdmn3 33043 ellkr 33394 diblss 35477 dihmeetlem4preN 35613 dihmeetlem13N 35626 pw2f1ocnv 36622 fvnonrel 36922 snhesn 37100 unirnmapsn 38401 sge0fodjrnlem 39309 1loopgrnb0 40717 umgr2v2enb1 40742 usgr2pthlem 40969 lindslinindsimp1 42040 |
Copyright terms: Public domain | W3C validator |