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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-sn 4589

This theorem is used by:  elsn  4599  elsni  4601  snidg  4622  elunsn  4645  eltpg  4648  el7g  4652  eldifsn  4750  sneqrg  4799  elsucg  6459  ltxr  13284  elfzp12  13777  fzdif1  13779  fprodn0f  16202  lcmfunsnlem2  16859  ramcl  17251  initoeu2lem1  18239  pmtrdifellem4  19744  psdmul  22542  plymulidp  26658  logbmpt  27173  2lgslem2  27779  xrge0tsmsbi  33734  rprmnz  34156  dimkerim  34370  elzrhunit  34720  esumrnmpt2  34811  bj-projval  38124  bj-elsn12g  38245  bj-elsnb  38246  bj-snmoore  38304  bj-elsn0  38344  eldmressnALTV  39477  brressn  39729  zndvdchrrhm  43289  aks4d1p6  43397  aks6d1c2lem4  43443  sticksstones11  43472  aks6d1c6lem2  43487  aks6d1c7lem1  43496  rhmqusspan  43501  unitscyglem2  43512  reclimc  46936  itgsincmulx  47257  dirkercncflem2  47387  dirkercncflem4  47389  fourierdlem53  47442  fourierdlem58  47447  fourierdlem60  47449  fourierdlem61  47450  fourierdlem62  47451  fourierdlem76  47465  fourierdlem101  47490  elaa2  47517  etransc  47566  qndenserrnbl  47578  sge0tsms  47663  el1fzopredsuc  48669  elclnbgrelnbgr  49196  clnbupgrel  49205  mndtcob  51051