Theorem elsng 4642

Description: There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15 (generalized). (Contributed by NM, 13-Sep-1995.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Assertion

Ref	Expression
elsng	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

Proof of Theorem elsng

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2736	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵))
2		df-sn 4629	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
3	1, 2	elab2g 3670	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {csn 4628

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sn 4629

This theorem is referenced by:  elsn  4643  elsni  4645  snidg  4662  eltpg  4689  eldifsn  4790  sneqrg  4840  elsucg  6432  ltxr  13099  elfzp12  13584  fprodn0f  15939  lcmfunsnlem2  16581  ramcl  16966  initoeu2lem1  17968  pmtrdifellem4  19388  logbmpt  26517  2lgslem2  27122  elunsn  32005  xrge0tsmsbi  32468  dimkerim  32988  elzrhunit  33245  esumrnmpt2  33352  plymulx  33845  bj-projval  36180  bj-elsn12g  36244  bj-elsnb  36245  bj-snmoore  36297  bj-elsn0  36339  eldmressnALTV  37443  brressn  37614  aks4d1p6  41252  sticksstones11  41278  metakunt20  41310  reclimc  44668  itgsincmulx  44989  dirkercncflem2  45119  dirkercncflem4  45121  fourierdlem53  45174  fourierdlem58  45179  fourierdlem60  45181  fourierdlem61  45182  fourierdlem62  45183  fourierdlem76  45197  fourierdlem101  45222  elaa2  45249  etransc  45298  qndenserrnbl  45310  sge0tsms  45395  el1fzopredsuc  46332  mndtcob  47796