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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-sn 4581

This theorem is referenced by:  elsn  4595  elsni  4597  snidg  4617  elunsn  4640  eltpg  4643  el7g  4647  eldifsn  4742  sneqrg  4795  elsucg  6387  ltxr  13029  elfzp12  13519  fzdif1  13521  fprodn0f  15914  lcmfunsnlem2  16567  ramcl  16957  initoeu2lem1  17938  pmtrdifellem4  19408  psdmul  22109  logbmpt  26754  2lgslem2  27362  xrge0tsmsbi  33156  rprmnz  33601  dimkerim  33784  elzrhunit  34134  esumrnmpt2  34225  plymulx  34705  bj-projval  37197  bj-elsn12g  37261  bj-elsnb  37262  bj-snmoore  37318  bj-elsn0  37360  eldmressnALTV  38472  brressn  38704  zndvdchrrhm  42226  aks4d1p6  42335  aks6d1c2lem4  42381  sticksstones11  42410  aks6d1c6lem2  42425  aks6d1c7lem1  42434  rhmqusspan  42439  unitscyglem2  42450  reclimc  45897  itgsincmulx  46218  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem53  46403  fourierdlem58  46408  fourierdlem60  46410  fourierdlem61  46411  fourierdlem62  46412  fourierdlem76  46426  fourierdlem101  46451  elaa2  46478  etransc  46527  qndenserrnbl  46539  sge0tsms  46624  el1fzopredsuc  47571  elclnbgrelnbgr  48071  clnbupgrel  48080  mndtcob  49827