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 4157 | . 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: fparlem1 7164 fparlem2 7165 el1o 7466 fin1a2lem11 9115 fin1a2lem12 9116 elnn0 11171 elxnn0 11242 elfzp1 12261 fsumss 14303 fprodss 14517 elhoma 16505 islpidl 19067 zrhrhmb 19678 rest0 20783 qustgphaus 21736 taylfval 23917 elch0 27495 atoml2i 28626 bj-eltag 32158 bj-rest10b 32223 dibopelvalN 35450 dibopelval2 35452 climrec 38670 |
Copyright terms: Public domain | W3C validator |