Theorem elsn2 4622

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  Vcvv 3440  {csn 4580

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-sn 4581

This theorem is referenced by:  fparlem1  8054  fparlem2  8055  el1o  8422  fin1a2lem11  10320  fin1a2lem12  10321  elnn0  12403  elxnn0  12476  elfzp1  13490  fsumss  15648  fprodss  15871  elhoma  17956  rnglidl0  21184  islpidl  21280  zrhrhmb  21465  rest0  23113  qustgphaus  24067  taylfval  26322  eqcuts3  27800  elch0  31329  atoml2i  32458  prmidl0  33531  bj-eltag  37178  bj-rest10b  37294  dibopelvalN  41403  dibopelval2  41405  aks4d1p1p4  42325  climrec  45849