Theorem elsn2 4631

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

Step	Hyp	Ref	Expression
1		elsn2.1	. 2 ⊢ 𝐵 ∈ V
2		elsn2g 4630	. 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)

Syntax hints:   ↔ wb 209   = wceq 1570   ∈ wcel 2143  Vcvv 3455  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-sn 4590

This theorem is referenced by:  fparlem1  8103  fparlem2  8104  el1o  8476  fin1a2lem11  10389  fin1a2lem12  10390  elnn0  12501  elxnn0  12574  elfzp1  13598  fsumss  15772  fprodss  15998  elhoma  18084  rnglidl0  21355  prmidl0  21478  islpidl  21493  zrhrhmb  21660  rest0  23326  qustgphaus  24280  taylfval  26522  eqcuts3  27997  elch0  31606  atoml2i  32735  bj-eltag  37633  bj-rest10b  37751  dibopelvalN  41937  dibopelval2  41939  aks4d1p1p4  42858  climrec  46339