Theorem elsng 4640

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  {csn 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sn 4627

This theorem is referenced by:  elsn  4641  elsni  4643  snidg  4660  elunsn  4683  eltpg  4686  el7g  4690  eldifsn  4786  sneqrg  4839  elsucg  6452  ltxr  13157  elfzp12  13643  fzdif1  13645  fprodn0f  16027  lcmfunsnlem2  16677  ramcl  17067  initoeu2lem1  18059  pmtrdifellem4  19497  psdmul  22170  logbmpt  26831  2lgslem2  27439  xrge0tsmsbi  33066  rprmnz  33548  dimkerim  33678  elzrhunit  33978  esumrnmpt2  34069  plymulx  34563  bj-projval  36997  bj-elsn12g  37061  bj-elsnb  37062  bj-snmoore  37114  bj-elsn0  37156  eldmressnALTV  38273  brressn  38442  zndvdchrrhm  41972  aks4d1p6  42082  aks6d1c2lem4  42128  sticksstones11  42157  aks6d1c6lem2  42172  aks6d1c7lem1  42181  rhmqusspan  42186  unitscyglem2  42197  metakunt20  42225  reclimc  45668  itgsincmulx  45989  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem53  46174  fourierdlem58  46179  fourierdlem60  46181  fourierdlem61  46182  fourierdlem62  46183  fourierdlem76  46197  fourierdlem101  46222  elaa2  46249  etransc  46298  qndenserrnbl  46310  sge0tsms  46395  el1fzopredsuc  47337  elclnbgrelnbgr  47812  clnbupgrel  47821  mndtcob  49179