Theorem elsn2 4636

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

Syntax hints:   ↔ wb 209   = wceq 1567   ∈ wcel 2149  Vcvv 3463  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-sn 4595

This theorem is referenced by:  fparlem1  8107  fparlem2  8108  el1o  8480  fin1a2lem11  10394  fin1a2lem12  10395  elnn0  12506  elxnn0  12579  elfzp1  13602  fsumss  15776  fprodss  16002  elhoma  18089  rnglidl0  21333  prmidl0  21447  islpidl  21462  zrhrhmb  21629  rest0  23295  qustgphaus  24249  taylfval  26488  eqcuts3  27963  elch0  31547  atoml2i  32676  bj-eltag  37501  bj-rest10b  37619  dibopelvalN  41807  dibopelval2  41809  aks4d1p1p4  42728  climrec  46211