Theorem elsng 4592

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

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

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-sn 4579

This theorem is referenced by:  elsn  4593  elsni  4595  snidg  4615  elunsn  4638  eltpg  4641  el7g  4645  eldifsn  4740  sneqrg  4793  elsucg  6385  ltxr  13027  elfzp12  13517  fzdif1  13519  fprodn0f  15912  lcmfunsnlem2  16565  ramcl  16955  initoeu2lem1  17936  pmtrdifellem4  19406  psdmul  22107  logbmpt  26752  2lgslem2  27360  xrge0tsmsbi  33105  rprmnz  33550  dimkerim  33733  elzrhunit  34083  esumrnmpt2  34174  plymulx  34654  bj-projval  37140  bj-elsn12g  37204  bj-elsnb  37205  bj-snmoore  37257  bj-elsn0  37299  eldmressnALTV  38411  brressn  38643  zndvdchrrhm  42165  aks4d1p6  42274  aks6d1c2lem4  42320  sticksstones11  42349  aks6d1c6lem2  42364  aks6d1c7lem1  42373  rhmqusspan  42378  unitscyglem2  42389  reclimc  45839  itgsincmulx  46160  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem53  46345  fourierdlem58  46350  fourierdlem60  46352  fourierdlem61  46353  fourierdlem62  46354  fourierdlem76  46368  fourierdlem101  46393  elaa2  46420  etransc  46469  qndenserrnbl  46481  sge0tsms  46566  el1fzopredsuc  47513  elclnbgrelnbgr  48013  clnbupgrel  48022  mndtcob  49769