Theorem elsn2 4670

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∈ wcel 2106  Vcvv 3478  {csn 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sn 4632

This theorem is referenced by:  fparlem1  8136  fparlem2  8137  el1o  8532  fin1a2lem11  10448  fin1a2lem12  10449  elnn0  12526  elxnn0  12599  elfzp1  13611  fsumss  15758  fprodss  15981  elhoma  18086  rnglidl0  21257  islpidl  21353  zrhrhmb  21539  rest0  23193  qustgphaus  24147  taylfval  26415  elch0  31283  atoml2i  32412  prmidl0  33458  bj-eltag  36960  bj-rest10b  37072  dibopelvalN  41126  dibopelval2  41128  aks4d1p1p4  42053  climrec  45559