![]() |
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 4644 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1533 ∈ wcel 2098 Vcvv 3461 {csn 4630 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-sn 4631 |
This theorem is referenced by: velsn 4646 opthwiener 5516 brsnop 5524 opthprc 5742 dmsnn0 6213 dmsnopg 6219 cnvcnvsn 6225 snsn0non 6496 funconstss 7064 fniniseg 7068 fniniseg2 7070 fsn 7144 fconstfv 7224 eusvobj2 7411 fnse 8138 xpord2pred 8150 xpord2indlem 8152 wfrlem14OLD 8343 fisn 9452 axdc3lem4 10478 axdc4lem 10480 axcclem 10482 opelreal 11155 seqid3 14047 seqz 14051 1exp 14092 hashf1lem2 14453 fprodn0f 15971 imasaddfnlem 17513 initoid 17993 termoid 17994 0subm 18777 smndex1mgm 18867 smndex1n0mnd 18872 grpinvfval 18943 0subg 19114 0subgOLD 19115 0nsg 19132 eqg0subg 19159 kerf1ghm 19210 sylow2alem2 19585 gsumval3 19874 gsumzaddlem 19888 lsssn0 20844 rngqiprngimf1 21207 pzriprnglem8 21431 r0cld 23686 alexsubALTlem2 23996 tgphaus 24065 isusp 24210 i1f1lem 25662 ig1pcl 26158 plyco0 26171 plyeq0lem 26189 plycj 26257 wilthlem2 27046 dchrfi 27233 mulsval 28059 snstriedgval 28923 incistruhgr 28964 1loopgrnb0 29388 umgr2v2enb1 29412 usgr2pthlem 29649 hsn0elch 31130 h1de2ctlem 31437 atomli 32264 suppiniseg 32548 1stpreimas 32567 gsummpt2d 32853 kerunit 33133 qqhval2lem 33713 qqhf 33718 qqhre 33752 esum2dlem 33842 eulerpartlemb 34119 bnj149 34637 subfacp1lem6 34926 ellimits 35637 bj-0nel1 36563 bj-isrvec 36904 poimirlem18 37242 poimirlem21 37245 poimirlem22 37246 poimirlem31 37255 poimirlem32 37256 itg2addnclem2 37276 ftc1anclem3 37299 0idl 37629 keridl 37636 smprngopr 37656 isdmn3 37678 ellkr 38691 diblss 40773 dihmeetlem4preN 40909 dihmeetlem13N 40922 sticksstones11 41759 0prjspnrel 42186 pw2f1ocnv 42600 fvnonrel 43169 snhesn 43358 unirnmapsn 44726 sge0fodjrnlem 45942 lindslinindsimp1 47711 |
Copyright terms: Public domain | W3C validator |