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

Theorem elsn2 4552
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 4551 . 2 (𝐵 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
31, 2ax-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