Theorem elsn2 4687

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∈ wcel 2108  Vcvv 3488  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sn 4649

This theorem is referenced by:  fparlem1  8153  fparlem2  8154  el1o  8551  fin1a2lem11  10479  fin1a2lem12  10480  elnn0  12555  elxnn0  12627  elfzp1  13634  fsumss  15773  fprodss  15996  elhoma  18099  rnglidl0  21262  islpidl  21358  zrhrhmb  21544  rest0  23198  qustgphaus  24152  taylfval  26418  elch0  31286  atoml2i  32415  prmidl0  33443  bj-eltag  36943  bj-rest10b  37055  dibopelvalN  41100  dibopelval2  41102  aks4d1p1p4  42028  climrec  45524