Theorem elsn2 4667

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106  Vcvv 3474  {csn 4628

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sn 4629

This theorem is referenced by:  fparlem1  8097  fparlem2  8098  el1o  8494  fin1a2lem11  10404  fin1a2lem12  10405  elnn0  12473  elxnn0  12545  elfzp1  13550  fsumss  15670  fprodss  15891  elhoma  17981  islpidl  20883  zrhrhmb  21059  rest0  22672  qustgphaus  23626  taylfval  25870  elch0  30502  atoml2i  31631  prmidl0  32564  bj-eltag  35853  bj-rest10b  35965  dibopelvalN  40009  dibopelval2  40011  aks4d1p1p4  40931  climrec  44309  rnglidl0  46742