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 207   = wceq 1547   ∈ wcel 2119  Vcvv 3431  {csn 4555

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 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-sn 4556

This theorem is referenced by:  fparlem1  8051  fparlem2  8052  el1o  8420  fin1a2lem11  10323  fin1a2lem12  10324  elnn0  12430  elxnn0  12503  elfzp1  13519  fsumss  15678  fprodss  15904  elhoma  17990  rnglidl0  21222  islpidl  21318  zrhrhmb  21485  rest0  23152  qustgphaus  24106  taylfval  26342  eqcuts3  27814  elch0  31343  atoml2i  32472  prmidl0  33533  bj-eltag  37330  bj-rest10b  37447  dibopelvalN  41635  dibopelval2  41637  aks4d1p1p4  42556  climrec  46048