![]() |
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 4665 | . 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1541 ∈ wcel 2106 Vcvv 3474 {csn 4627 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-sn 4628 |
This theorem is referenced by: fparlem1 8094 fparlem2 8095 el1o 8491 fin1a2lem11 10401 fin1a2lem12 10402 elnn0 12470 elxnn0 12542 elfzp1 13547 fsumss 15667 fprodss 15888 elhoma 17978 islpidl 20876 zrhrhmb 21051 rest0 22664 qustgphaus 23618 taylfval 25862 elch0 30494 atoml2i 31623 prmidl0 32557 bj-eltag 35846 bj-rest10b 35958 dibopelvalN 40002 dibopelval2 40004 aks4d1p1p4 40924 climrec 44305 rnglidl0 46734 |
Copyright terms: Public domain | W3C validator |