Theorem elsn2 4401

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

Syntax hints:   ↔ wb 198   = wceq 1653   ∈ wcel 2157  Vcvv 3383  {csn 4366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-v 3385  df-sn 4367

This theorem is referenced by:  fparlem1  7512  fparlem2  7513  el1o  7817  fin1a2lem11  9518  fin1a2lem12  9519  elnn0  11578  elxnn0  11650  elfzp1  12641  fsumss  14793  fprodss  15011  elhoma  16992  islpidl  19565  zrhrhmb  20177  rest0  21298  qustgphaus  22250  taylfval  24450  elch0  28627  atoml2i  29758  bj-eltag  33448  bj-rest10b  33526  dibopelvalN  37155  dibopelval2  37157  climrec  40566