Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elsn2 Structured version   Visualization version   GIF version

Theorem elsn2 4596
 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.)
Hypothesis
Ref Expression
elsn2.1 𝐵 ∈ V
Assertion
Ref Expression
elsn2 (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)

Proof of Theorem elsn2
StepHypRef Expression
1 elsn2.1 . 2 𝐵 ∈ V
2 elsn2g 4595 . 2 (𝐵 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   = wceq 1530   ∈ wcel 2107  Vcvv 3493  {csn 4559 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-sn 4560 This theorem is referenced by:  fparlem1  7799  fparlem2  7800  el1o  8116  fin1a2lem11  9824  fin1a2lem12  9825  elnn0  11891  elxnn0  11961  elfzp1  12949  fsumss  15074  fprodss  15294  elhoma  17284  islpidl  20011  zrhrhmb  20650  rest0  21769  qustgphaus  22723  taylfval  24939  elch0  29023  atoml2i  30152  bj-eltag  34277  bj-rest10b  34367  dibopelvalN  38266  dibopelval2  38268  climrec  41868
 Copyright terms: Public domain W3C validator