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

Theorem elsn2 4666
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 4665 . 2 (𝐵 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1541  wcel 2106  Vcvv 3474  {csn 4627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sn 4628
This theorem is referenced by:  fparlem1  8094  fparlem2  8095  el1o  8491  fin1a2lem11  10401  fin1a2lem12  10402  elnn0  12470  elxnn0  12542  elfzp1  13547  fsumss  15667  fprodss  15888  elhoma  17978  islpidl  20876  zrhrhmb  21051  rest0  22664  qustgphaus  23618  taylfval  25862  elch0  30494  atoml2i  31623  prmidl0  32557  bj-eltag  35846  bj-rest10b  35958  dibopelvalN  40002  dibopelval2  40004  aks4d1p1p4  40924  climrec  44305  rnglidl0  46734
  Copyright terms: Public domain W3C validator