Theorem elsn2 4664

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

Syntax hints:   ↔ wb 206   = wceq 1539   ∈ wcel 2107  Vcvv 3479  {csn 4625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-sn 4626

This theorem is referenced by:  fparlem1  8138  fparlem2  8139  el1o  8534  fin1a2lem11  10451  fin1a2lem12  10452  elnn0  12530  elxnn0  12603  elfzp1  13615  fsumss  15762  fprodss  15985  elhoma  18078  rnglidl0  21240  islpidl  21336  zrhrhmb  21522  rest0  23178  qustgphaus  24132  taylfval  26401  elch0  31274  atoml2i  32403  prmidl0  33479  bj-eltag  36979  bj-rest10b  37091  dibopelvalN  41146  dibopelval2  41148  aks4d1p1p4  42073  climrec  45623