Theorem elsn2 4624

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

Syntax hints:   ↔ wb 208   = wceq 1560   ∈ wcel 2142  Vcvv 3454  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-sn 4583

This theorem is referenced by:  fparlem1  8091  fparlem2  8092  el1o  8464  fin1a2lem11  10367  fin1a2lem12  10368  elnn0  12483  elxnn0  12556  elfzp1  13579  fsumss  15752  fprodss  15978  elhoma  18065  rnglidl0  21299  islpidl  21395  zrhrhmb  21562  rest0  23229  qustgphaus  24183  taylfval  26422  eqcuts3  27897  elch0  31457  atoml2i  32586  prmidl0  33637  bj-eltag  37462  bj-rest10b  37579  dibopelvalN  41767  dibopelval2  41769  aks4d1p1p4  42688  climrec  46179