Theorem elsn2 4629

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  Vcvv 3447  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sn 4590

This theorem is referenced by:  fparlem1  8091  fparlem2  8092  el1o  8459  fin1a2lem11  10363  fin1a2lem12  10364  elnn0  12444  elxnn0  12517  elfzp1  13535  fsumss  15691  fprodss  15914  elhoma  17994  rnglidl0  21139  islpidl  21235  zrhrhmb  21420  rest0  23056  qustgphaus  24010  taylfval  26266  elch0  31183  atoml2i  32312  prmidl0  33421  bj-eltag  36965  bj-rest10b  37077  dibopelvalN  41137  dibopelval2  41139  aks4d1p1p4  42059  climrec  45601