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 4599 | . 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1539 ∈ wcel 2106 Vcvv 3432 {csn 4561 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-sn 4562 |
This theorem is referenced by: fparlem1 7952 fparlem2 7953 el1o 8325 fin1a2lem11 10166 fin1a2lem12 10167 elnn0 12235 elxnn0 12307 elfzp1 13306 fsumss 15437 fprodss 15658 elhoma 17747 islpidl 20517 zrhrhmb 20712 rest0 22320 qustgphaus 23274 taylfval 25518 elch0 29616 atoml2i 30745 prmidl0 31626 bj-eltag 35167 bj-rest10b 35260 dibopelvalN 39157 dibopelval2 39159 aks4d1p1p4 40079 climrec 43144 |
Copyright terms: Public domain | W3C validator |