Theorem elsn2 4633

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146  Vcvv 3457  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-sn 4592

This theorem is used by:  fparlem1  8113  fparlem2  8114  el1o  8486  fin1a2lem11  10409  fin1a2lem12  10410  elnn0  12523  elxnn0  12596  elfzp1  13621  fsumss  15801  fprodss  16027  elhoma  18113  rnglidl0  21407  prmidl0  21530  islpidl  21545  zrhrhmb  21712  rest0  23378  qustgphaus  24333  taylfval  26575  eqcuts3  28050  elch0  31679  atoml2i  32808  bj-eltag  37672  bj-rest10b  37790  dibopelvalN  41977  dibopelval2  41979  aks4d1p1p4  42898  climrec  46379