Theorem elsn2 4620

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  Vcvv 3438  {csn 4578

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-sn 4579

This theorem is referenced by:  fparlem1  8052  fparlem2  8053  el1o  8420  fin1a2lem11  10318  fin1a2lem12  10319  elnn0  12401  elxnn0  12474  elfzp1  13488  fsumss  15646  fprodss  15869  elhoma  17954  rnglidl0  21182  islpidl  21278  zrhrhmb  21463  rest0  23111  qustgphaus  24065  taylfval  26320  eqscut3  27792  elch0  31278  atoml2i  32407  prmidl0  33480  bj-eltag  37121  bj-rest10b  37233  dibopelvalN  41342  dibopelval2  41344  aks4d1p1p4  42264  climrec  45791