Theorem elsn2 4564

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

Syntax hints:   ↔ wb 209   = wceq 1538   ∈ wcel 2111  Vcvv 3441  {csn 4525

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sn 4526

This theorem is referenced by:  fparlem1  7790  fparlem2  7791  el1o  8107  fin1a2lem11  9821  fin1a2lem12  9822  elnn0  11887  elxnn0  11957  elfzp1  12952  fsumss  15074  fprodss  15294  elhoma  17284  islpidl  20012  zrhrhmb  20204  rest0  21774  qustgphaus  22728  taylfval  24954  elch0  29037  atoml2i  30166  prmidl0  31034  bj-eltag  34413  bj-rest10b  34504  dibopelvalN  38439  dibopelval2  38441  climrec  42245