Theorem elsng 4608

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 2773	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵))
2		df-sn 4595	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
3	1, 2	elab2g 3648	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-sn 4595

This theorem is referenced by:  elsn  4609  elsni  4611  snidg  4631  elunsn  4654  eltpg  4657  el7g  4661  eldifsn  4758  sneqrg  4808  elsucg  6432  ltxr  13139  elfzp12  13630  fzdif1  13632  fprodn0f  16044  lcmfunsnlem2  16697  ramcl  17088  initoeu2lem1  18070  pmtrdifellem4  19548  psdmul  22297  plymulidp  26411  logbmpt  26918  2lgslem2  27524  xrge0tsmsbi  33334  rprmnz  33754  dimkerim  33961  elzrhunit  34311  esumrnmpt2  34402  bj-projval  37519  bj-elsn12g  37583  bj-elsnb  37584  bj-snmoore  37642  bj-elsn0  37686  eldmressnALTV  38817  brressn  39069  zndvdchrrhm  42629  aks4d1p6  42737  aks6d1c2lem4  42783  sticksstones11  42812  aks6d1c6lem2  42827  aks6d1c7lem1  42836  rhmqusspan  42841  unitscyglem2  42852  reclimc  46258  itgsincmulx  46579  dirkercncflem2  46709  dirkercncflem4  46711  fourierdlem53  46764  fourierdlem58  46769  fourierdlem60  46771  fourierdlem61  46772  fourierdlem62  46773  fourierdlem76  46787  fourierdlem101  46812  elaa2  46839  etransc  46888  qndenserrnbl  46900  sge0tsms  46985  el1fzopredsuc  47951  elclnbgrelnbgr  48478  clnbupgrel  48487  mndtcob  50244