Theorem elsng 4615

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sn 4602

This theorem is referenced by:  elsn  4616  elsni  4618  snidg  4636  elunsn  4659  eltpg  4662  el7g  4666  eldifsn  4762  sneqrg  4815  elsucg  6422  ltxr  13131  elfzp12  13620  fzdif1  13622  fprodn0f  16007  lcmfunsnlem2  16659  ramcl  17049  initoeu2lem1  18027  pmtrdifellem4  19460  psdmul  22104  logbmpt  26750  2lgslem2  27358  xrge0tsmsbi  33057  rprmnz  33535  dimkerim  33667  elzrhunit  34008  esumrnmpt2  34099  plymulx  34580  bj-projval  37014  bj-elsn12g  37078  bj-elsnb  37079  bj-snmoore  37131  bj-elsn0  37173  eldmressnALTV  38290  brressn  38459  zndvdchrrhm  41985  aks4d1p6  42094  aks6d1c2lem4  42140  sticksstones11  42169  aks6d1c6lem2  42184  aks6d1c7lem1  42193  rhmqusspan  42198  unitscyglem2  42209  metakunt20  42237  reclimc  45682  itgsincmulx  46003  dirkercncflem2  46133  dirkercncflem4  46135  fourierdlem53  46188  fourierdlem58  46193  fourierdlem60  46195  fourierdlem61  46196  fourierdlem62  46197  fourierdlem76  46211  fourierdlem101  46236  elaa2  46263  etransc  46312  qndenserrnbl  46324  sge0tsms  46409  el1fzopredsuc  47354  elclnbgrelnbgr  47839  clnbupgrel  47848  mndtcob  49459