Theorem elsn2 4552

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

Syntax hints:   ↔ wb 209   = wceq 1542   ∈ wcel 2113  Vcvv 3397  {csn 4513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-sn 4514

This theorem is referenced by:  fparlem1  7826  fparlem2  7827  el1o  8148  fin1a2lem11  9903  fin1a2lem12  9904  elnn0  11971  elxnn0  12043  elfzp1  13041  fsumss  15168  fprodss  15387  elhoma  17397  islpidl  20131  zrhrhmb  20324  rest0  21913  qustgphaus  22867  taylfval  25098  elch0  29181  atoml2i  30310  prmidl0  31190  bj-eltag  34779  bj-rest10b  34870  dibopelvalN  38769  dibopelval2  38771  aks4d1p1p4  39687  climrec  42670