Theorem elsng 4603

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sn 4590

This theorem is referenced by:  elsn  4604  elsni  4606  snidg  4624  elunsn  4647  eltpg  4650  el7g  4654  eldifsn  4750  sneqrg  4803  elsucg  6402  ltxr  13075  elfzp12  13564  fzdif1  13566  fprodn0f  15957  lcmfunsnlem2  16610  ramcl  17000  initoeu2lem1  17976  pmtrdifellem4  19409  psdmul  22053  logbmpt  26698  2lgslem2  27306  xrge0tsmsbi  33003  rprmnz  33491  dimkerim  33623  elzrhunit  33967  esumrnmpt2  34058  plymulx  34539  bj-projval  36984  bj-elsn12g  37048  bj-elsnb  37049  bj-snmoore  37101  bj-elsn0  37143  eldmressnALTV  38261  brressn  38432  zndvdchrrhm  41960  aks4d1p6  42069  aks6d1c2lem4  42115  sticksstones11  42144  aks6d1c6lem2  42159  aks6d1c7lem1  42168  rhmqusspan  42173  unitscyglem2  42184  reclimc  45651  itgsincmulx  45972  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem53  46157  fourierdlem58  46162  fourierdlem60  46164  fourierdlem61  46165  fourierdlem62  46166  fourierdlem76  46180  fourierdlem101  46205  elaa2  46232  etransc  46281  qndenserrnbl  46293  sge0tsms  46378  el1fzopredsuc  47326  elclnbgrelnbgr  47826  clnbupgrel  47835  mndtcob  49571