Theorem elsn2 4597

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2108  Vcvv 3422  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sn 4559

This theorem is referenced by:  fparlem1  7923  fparlem2  7924  el1o  8291  fin1a2lem11  10097  fin1a2lem12  10098  elnn0  12165  elxnn0  12237  elfzp1  13235  fsumss  15365  fprodss  15586  elhoma  17663  islpidl  20430  zrhrhmb  20624  rest0  22228  qustgphaus  23182  taylfval  25423  elch0  29517  atoml2i  30646  prmidl0  31528  bj-eltag  35094  bj-rest10b  35187  dibopelvalN  39084  dibopelval2  39086  aks4d1p1p4  40007  climrec  43034