Theorem elsn2 4356

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

Syntax hints:   ↔ wb 196   = wceq 1632   ∈ wcel 2139  Vcvv 3340  {csn 4321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-sn 4322

This theorem is referenced by:  fparlem1  7445  fparlem2  7446  el1o  7748  fin1a2lem11  9424  fin1a2lem12  9425  elnn0  11486  elxnn0  11557  elfzp1  12584  fsumss  14655  fprodss  14877  elhoma  16883  islpidl  19448  zrhrhmb  20061  rest0  21175  qustgphaus  22127  taylfval  24312  elch0  28420  atoml2i  29551  bj-eltag  33271  bj-rest10b  33348  dibopelvalN  36934  dibopelval2  36936  climrec  40338