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 4551 | . 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1542 ∈ wcel 2113 Vcvv 3397 {csn 4513 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-sn 4514 |
This theorem is referenced by: fparlem1 7826 fparlem2 7827 el1o 8148 fin1a2lem11 9903 fin1a2lem12 9904 elnn0 11971 elxnn0 12043 elfzp1 13041 fsumss 15168 fprodss 15387 elhoma 17397 islpidl 20131 zrhrhmb 20324 rest0 21913 qustgphaus 22867 taylfval 25098 elch0 29181 atoml2i 30310 prmidl0 31190 bj-eltag 34779 bj-rest10b 34870 dibopelvalN 38769 dibopelval2 38771 aks4d1p1p4 39687 climrec 42670 |
Copyright terms: Public domain | W3C validator |