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

Theorem elsn2 4664
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 4663 . 2 (𝐵 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1539  wcel 2107  Vcvv 3479  {csn 4625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-sn 4626
This theorem is referenced by:  fparlem1  8138  fparlem2  8139  el1o  8534  fin1a2lem11  10451  fin1a2lem12  10452  elnn0  12530  elxnn0  12603  elfzp1  13615  fsumss  15762  fprodss  15985  elhoma  18078  rnglidl0  21240  islpidl  21336  zrhrhmb  21522  rest0  23178  qustgphaus  24132  taylfval  26401  elch0  31274  atoml2i  32403  prmidl0  33479  bj-eltag  36979  bj-rest10b  37091  dibopelvalN  41146  dibopelval2  41148  aks4d1p1p4  42073  climrec  45623
  Copyright terms: Public domain W3C validator