Theorem elsn2 4606

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

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114  Vcvv 3496  {csn 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-sn 4570

This theorem is referenced by:  fparlem1  7809  fparlem2  7810  el1o  8126  fin1a2lem11  9834  fin1a2lem12  9835  elnn0  11902  elxnn0  11972  elfzp1  12960  fsumss  15084  fprodss  15304  elhoma  17294  islpidl  20021  zrhrhmb  20660  rest0  21779  qustgphaus  22733  taylfval  24949  elch0  29033  atoml2i  30162  bj-eltag  34291  bj-rest10b  34382  dibopelvalN  38281  dibopelval2  38283  climrec  41891