Theorem elsng 4587

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

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

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-sn 4574

This theorem is referenced by:  elsn  4588  elsni  4590  snidg  4610  elunsn  4633  eltpg  4636  el7g  4640  eldifsn  4735  sneqrg  4788  elsucg  6376  ltxr  13014  elfzp12  13503  fzdif1  13505  fprodn0f  15898  lcmfunsnlem2  16551  ramcl  16941  initoeu2lem1  17921  pmtrdifellem4  19391  psdmul  22081  logbmpt  26725  2lgslem2  27333  xrge0tsmsbi  33043  rprmnz  33485  dimkerim  33640  elzrhunit  33990  esumrnmpt2  34081  plymulx  34561  bj-projval  37038  bj-elsn12g  37102  bj-elsnb  37103  bj-snmoore  37155  bj-elsn0  37197  eldmressnALTV  38315  brressn  38486  zndvdchrrhm  42013  aks4d1p6  42122  aks6d1c2lem4  42168  sticksstones11  42197  aks6d1c6lem2  42212  aks6d1c7lem1  42221  rhmqusspan  42226  unitscyglem2  42237  reclimc  45699  itgsincmulx  46020  dirkercncflem2  46150  dirkercncflem4  46152  fourierdlem53  46205  fourierdlem58  46210  fourierdlem60  46212  fourierdlem61  46213  fourierdlem62  46214  fourierdlem76  46228  fourierdlem101  46253  elaa2  46280  etransc  46329  qndenserrnbl  46341  sge0tsms  46426  el1fzopredsuc  47364  elclnbgrelnbgr  47864  clnbupgrel  47873  mndtcob  49622