Theorem elsng 4662

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sn 4649

This theorem is referenced by:  elsn  4663  elsni  4665  snidg  4682  eltpg  4709  el7g  4713  eldifsn  4811  sneqrg  4864  elsucg  6463  ltxr  13178  elfzp12  13663  fprodn0f  16039  lcmfunsnlem2  16687  ramcl  17076  initoeu2lem1  18081  pmtrdifellem4  19521  psdmul  22193  logbmpt  26849  2lgslem2  27457  elunsn  32541  xrge0tsmsbi  33042  rprmnz  33513  dimkerim  33640  elzrhunit  33925  esumrnmpt2  34032  plymulx  34525  bj-projval  36962  bj-elsn12g  37026  bj-elsnb  37027  bj-snmoore  37079  bj-elsn0  37121  eldmressnALTV  38228  brressn  38397  zndvdchrrhm  41927  aks4d1p6  42038  aks6d1c2lem4  42084  sticksstones11  42113  aks6d1c6lem2  42128  aks6d1c7lem1  42137  rhmqusspan  42142  unitscyglem2  42153  metakunt20  42181  reclimc  45574  itgsincmulx  45895  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem53  46080  fourierdlem58  46085  fourierdlem60  46087  fourierdlem61  46088  fourierdlem62  46089  fourierdlem76  46103  fourierdlem101  46128  elaa2  46155  etransc  46204  qndenserrnbl  46216  sge0tsms  46301  el1fzopredsuc  47240  clnbupgrel  47707  mndtcob  48755