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 206   = wceq 1542   ∈ wcel 2114  Vcvv 3442  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sn 4583

This theorem is referenced by:  fparlem1  8064  fparlem2  8065  el1o  8432  fin1a2lem11  10332  fin1a2lem12  10333  elnn0  12415  elxnn0  12488  elfzp1  13502  fsumss  15660  fprodss  15883  elhoma  17968  rnglidl0  21196  islpidl  21292  zrhrhmb  21477  rest0  23125  qustgphaus  24079  taylfval  26334  eqcuts3  27812  elch0  31342  atoml2i  32471  prmidl0  33543  bj-eltag  37225  bj-rest10b  37342  dibopelvalN  41519  dibopelval2  41521  aks4d1p1p4  42441  climrec  45963