Theorem elsng 4594

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sn 4585

This theorem is used by:  elsn  4595  elsni  4597  snidg  4617  elunsn  4640  eltpg  4643  el7g  4647  eldifsn  4744  sneqrg  4793  elsucg  6436  ltxr  13251  elfzp12  13744  fzdif1  13746  fprodn0f  16167  lcmfunsnlem2  16824  ramcl  17216  initoeu2lem1  18198  pmtrdifellem4  19702  psdmul  22496  plymulidp  26612  logbmpt  27125  2lgslem2  27731  xrge0tsmsbi  33685  rprmnz  34102  dimkerim  34309  elzrhunit  34659  esumrnmpt2  34750  bj-projval  38005  bj-elsn12g  38083  bj-elsnb  38084  bj-snmoore  38142  bj-elsn0  38185  eldmressnALTV  39320  brressn  39572  zndvdchrrhm  43132  aks4d1p6  43240  aks6d1c2lem4  43286  sticksstones11  43315  aks6d1c6lem2  43330  aks6d1c7lem1  43339  rhmqusspan  43344  unitscyglem2  43355  reclimc  46771  itgsincmulx  47092  dirkercncflem2  47222  dirkercncflem4  47224  fourierdlem53  47277  fourierdlem58  47282  fourierdlem60  47284  fourierdlem61  47285  fourierdlem62  47286  fourierdlem76  47300  fourierdlem101  47325  elaa2  47352  etransc  47401  qndenserrnbl  47413  sge0tsms  47498  el1fzopredsuc  48504  elclnbgrelnbgr  49031  clnbupgrel  49040  mndtcob  50828