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

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