Theorem elsn2 4604

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

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114  Vcvv 3494  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-sn 4568

This theorem is referenced by:  fparlem1  7807  fparlem2  7808  el1o  8124  fin1a2lem11  9832  fin1a2lem12  9833  elnn0  11900  elxnn0  11970  elfzp1  12958  fsumss  15082  fprodss  15302  elhoma  17292  islpidl  20019  zrhrhmb  20658  rest0  21777  qustgphaus  22731  taylfval  24947  elch0  29031  atoml2i  30160  bj-eltag  34292  bj-rest10b  34383  dibopelvalN  38294  dibopelval2  38296  climrec  41904