Theorem elsn2 4668

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 4667	. 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2107  Vcvv 3475  {csn 4629

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sn 4630

This theorem is referenced by:  fparlem1  8098  fparlem2  8099  el1o  8495  fin1a2lem11  10405  fin1a2lem12  10406  elnn0  12474  elxnn0  12546  elfzp1  13551  fsumss  15671  fprodss  15892  elhoma  17982  islpidl  20884  zrhrhmb  21060  rest0  22673  qustgphaus  23627  taylfval  25871  elch0  30507  atoml2i  31636  prmidl0  32569  bj-eltag  35858  bj-rest10b  35970  dibopelvalN  40014  dibopelval2  40016  aks4d1p1p4  40936  climrec  44319  rnglidl0  46752