Theorem elsn2 4615

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2111  Vcvv 3436  {csn 4573

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-sn 4574

This theorem is referenced by:  fparlem1  8042  fparlem2  8043  el1o  8410  fin1a2lem11  10301  fin1a2lem12  10302  elnn0  12383  elxnn0  12456  elfzp1  13474  fsumss  15632  fprodss  15855  elhoma  17939  rnglidl0  21166  islpidl  21262  zrhrhmb  21447  rest0  23084  qustgphaus  24038  taylfval  26293  eqscut3  27765  elch0  31234  atoml2i  32363  prmidl0  33415  bj-eltag  37021  bj-rest10b  37133  dibopelvalN  41252  dibopelval2  41254  aks4d1p1p4  42174  climrec  45713