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 4210 | . 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1483 ∈ wcel 1990 Vcvv 3200 {csn 4177 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-sn 4178 |
This theorem is referenced by: fparlem1 7277 fparlem2 7278 el1o 7579 fin1a2lem11 9232 fin1a2lem12 9233 elnn0 11294 elxnn0 11365 elfzp1 12391 fsumss 14456 fprodss 14678 elhoma 16682 islpidl 19246 zrhrhmb 19859 rest0 20973 qustgphaus 21926 taylfval 24113 elch0 28111 atoml2i 29242 bj-eltag 32965 bj-rest10b 33042 dibopelvalN 36432 dibopelval2 36434 climrec 39835 |
Copyright terms: Public domain | W3C validator |