Theorem elsn2 4626

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145  Vcvv 3451  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-sn 4585

This theorem is used by:  fparlem1  8123  fparlem2  8124  el1o  8503  fin1a2lem11  10488  fin1a2lem12  10489  elnn0  12608  elxnn0  12681  elfzp1  13708  fsumss  15891  fprodss  16115  elhoma  18207  rnglidl0  21509  prmidl0  21634  islpidl  21649  zrhrhmb  21816  rest0  23487  qustgphaus  24442  taylfval  26686  eqcuts3  28190  elch0  31856  atoml2i  32985  bj-eltag  37890  bj-rest10b  38010  dibopelvalN  42200  dibopelval2  42202  aks4d1p1p4  43121  climrec  46614  tmachlem-agreesn  47956