Theorem elsng 4569

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-sn 4556

This theorem is referenced by:  elsn  4570  elsni  4572  snidg  4592  elunsn  4615  eltpg  4618  el7g  4622  eldifsn  4719  sneqrg  4770  elsucg  6380  ltxr  13057  elfzp12  13548  fzdif1  13550  fprodn0f  15947  lcmfunsnlem2  16600  ramcl  16991  initoeu2lem1  17972  pmtrdifellem4  19445  psdmul  22154  logbmpt  26770  2lgslem2  27376  xrge0tsmsbi  33155  rprmnz  33603  dimkerim  33811  elzrhunit  34161  esumrnmpt2  34252  plymulx  34732  bj-projval  37349  bj-elsn12g  37413  bj-elsnb  37414  bj-snmoore  37471  bj-elsn0  37515  eldmressnALTV  38646  brressn  38898  zndvdchrrhm  42458  aks4d1p6  42566  aks6d1c2lem4  42612  sticksstones11  42641  aks6d1c6lem2  42656  aks6d1c7lem1  42665  rhmqusspan  42670  unitscyglem2  42681  reclimc  46096  itgsincmulx  46417  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem53  46602  fourierdlem58  46607  fourierdlem60  46609  fourierdlem61  46610  fourierdlem62  46611  fourierdlem76  46625  fourierdlem101  46650  elaa2  46677  etransc  46726  qndenserrnbl  46738  sge0tsms  46823  el1fzopredsuc  47789  elclnbgrelnbgr  48316  clnbupgrel  48325  mndtcob  50072