Theorem elsng 4598

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 3634	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sn 4585

This theorem is used by:  elsn  4599  elsni  4601  snidg  4621  elunsn  4644  eltpg  4647  el7g  4651  eldifsn  4748  sneqrg  4799  elsucg  6428  ltxr  13166  elfzp12  13658  fzdif1  13660  fprodn0f  16078  lcmfunsnlem2  16730  ramcl  17121  initoeu2lem1  18103  pmtrdifellem4  19606  psdmul  22394  plymulidp  26512  logbmpt  27025  2lgslem2  27631  xrge0tsmsbi  33514  rprmnz  33930  dimkerim  34137  elzrhunit  34487  esumrnmpt2  34578  bj-projval  37740  bj-elsn12g  37804  bj-elsnb  37805  bj-snmoore  37863  bj-elsn0  37907  eldmressnALTV  39027  brressn  39279  zndvdchrrhm  42839  aks4d1p6  42947  aks6d1c2lem4  42993  sticksstones11  43022  aks6d1c6lem2  43037  aks6d1c7lem1  43046  rhmqusspan  43051  unitscyglem2  43062  reclimc  46481  itgsincmulx  46802  dirkercncflem2  46932  dirkercncflem4  46934  fourierdlem53  46987  fourierdlem58  46992  fourierdlem60  46994  fourierdlem61  46995  fourierdlem62  46996  fourierdlem76  47010  fourierdlem101  47035  elaa2  47062  etransc  47111  qndenserrnbl  47123  sge0tsms  47208  el1fzopredsuc  48214  elclnbgrelnbgr  48741  clnbupgrel  48750  mndtcob  50508