Theorem elsng 4581

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-sn 4568

This theorem is referenced by:  elsn  4582  elsni  4584  snidg  4604  elunsn  4627  eltpg  4630  el7g  4634  eldifsn  4731  sneqrg  4782  elsucg  6393  ltxr  13066  elfzp12  13557  fzdif1  13559  fprodn0f  15956  lcmfunsnlem2  16609  ramcl  17000  initoeu2lem1  17981  pmtrdifellem4  19454  psdmul  22132  logbmpt  26752  2lgslem2  27358  xrge0tsmsbi  33135  rprmnz  33580  dimkerim  33771  elzrhunit  34121  esumrnmpt2  34212  plymulx  34692  bj-projval  37303  bj-elsn12g  37367  bj-elsnb  37368  bj-snmoore  37425  bj-elsn0  37469  eldmressnALTV  38600  brressn  38852  zndvdchrrhm  42412  aks4d1p6  42520  aks6d1c2lem4  42566  sticksstones11  42595  aks6d1c6lem2  42610  aks6d1c7lem1  42619  rhmqusspan  42624  unitscyglem2  42635  reclimc  46081  itgsincmulx  46402  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem53  46587  fourierdlem58  46592  fourierdlem60  46594  fourierdlem61  46595  fourierdlem62  46596  fourierdlem76  46610  fourierdlem101  46635  elaa2  46662  etransc  46711  qndenserrnbl  46723  sge0tsms  46808  el1fzopredsuc  47774  elclnbgrelnbgr  48301  clnbupgrel  48310  mndtcob  50057