Theorem elsn2 4623

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  Vcvv 3441  {csn 4581

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sn 4582

This theorem is referenced by:  fparlem1  8056  fparlem2  8057  el1o  8424  fin1a2lem11  10324  fin1a2lem12  10325  elnn0  12407  elxnn0  12480  elfzp1  13494  fsumss  15652  fprodss  15875  elhoma  17960  rnglidl0  21188  islpidl  21284  zrhrhmb  21469  rest0  23117  qustgphaus  24071  taylfval  26326  eqscut3  27802  elch0  31312  atoml2i  32441  prmidl0  33512  bj-eltag  37153  bj-rest10b  37265  dibopelvalN  41440  dibopelval2  41442  aks4d1p1p4  42362  climrec  45885