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

Theorem elsn2 4630
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 4629 . 2 (𝐵 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542  wcel 2107  Vcvv 3448  {csn 4591
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-sn 4592
This theorem is referenced by:  fparlem1  8049  fparlem2  8050  el1o  8446  fin1a2lem11  10353  fin1a2lem12  10354  elnn0  12422  elxnn0  12494  elfzp1  13498  fsumss  15617  fprodss  15838  elhoma  17925  islpidl  20732  zrhrhmb  20927  rest0  22536  qustgphaus  23490  taylfval  25734  elch0  30238  atoml2i  31367  prmidl0  32263  bj-eltag  35477  bj-rest10b  35589  dibopelvalN  39635  dibopelval2  39637  aks4d1p1p4  40557  climrec  43918
  Copyright terms: Public domain W3C validator