|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > elsn2 | Structured version Visualization version GIF version | ||
| Description: There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that 𝐵, rather than 𝐴, be a set. (Contributed by NM, 12-Jun-1994.) | 
| Ref | Expression | 
|---|---|
| elsn2.1 | ⊢ 𝐵 ∈ V | 
| Ref | Expression | 
|---|---|
| elsn2 | ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | elsn2.1 | . 2 ⊢ 𝐵 ∈ V | |
| 2 | elsn2g 4663 | . 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 = wceq 1539 ∈ wcel 2107 Vcvv 3479 {csn 4625 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-sn 4626 | 
| This theorem is referenced by: fparlem1 8138 fparlem2 8139 el1o 8534 fin1a2lem11 10451 fin1a2lem12 10452 elnn0 12530 elxnn0 12603 elfzp1 13615 fsumss 15762 fprodss 15985 elhoma 18078 rnglidl0 21240 islpidl 21336 zrhrhmb 21522 rest0 23178 qustgphaus 24132 taylfval 26401 elch0 31274 atoml2i 32403 prmidl0 33479 bj-eltag 36979 bj-rest10b 37091 dibopelvalN 41146 dibopelval2 41148 aks4d1p1p4 42073 climrec 45623 | 
| Copyright terms: Public domain | W3C validator |