Theorem elsn2 4609

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  Vcvv 3429  {csn 4567

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-sn 4568

This theorem is referenced by:  fparlem1  8062  fparlem2  8063  el1o  8430  fin1a2lem11  10332  fin1a2lem12  10333  elnn0  12439  elxnn0  12512  elfzp1  13528  fsumss  15687  fprodss  15913  elhoma  17999  rnglidl0  21227  islpidl  21323  zrhrhmb  21490  rest0  23134  qustgphaus  24088  taylfval  26324  eqcuts3  27796  elch0  31325  atoml2i  32454  prmidl0  33510  bj-eltag  37284  bj-rest10b  37401  dibopelvalN  41589  dibopelval2  41591  aks4d1p1p4  42510  climrec  46033