Theorem elsng 4584

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1536   ∈ wcel 2113  {csn 4570

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-sn 4571

This theorem is referenced by:  elsn  4585  elsni  4587  snidg  4602  eltpg  4626  eldifsn  4722  eldifsnneqOLD  4727  sneqrg  4773  elsucg  6261  ltxr  12513  elfzp12  12989  fprodn0f  15348  lcmfunsnlem2  15987  ramcl  16368  initoeu2lem1  17277  pmtrdifellem4  18610  logbmpt  25369  2lgslem2  25974  elunsn  30276  xrge0tsmsbi  30697  dimkerim  31027  elzrhunit  31224  esumrnmpt2  31331  plymulx  31822  bj-projval  34312  bj-elsn12g  34357  bj-elsnb  34358  bj-snmoore  34409  bj-elsn0  34451  reclimc  41940  itgsincmulx  42265  dirkercncflem2  42396  dirkercncflem4  42398  fourierdlem53  42451  fourierdlem58  42456  fourierdlem60  42458  fourierdlem61  42459  fourierdlem62  42460  fourierdlem76  42474  fourierdlem101  42499  elaa2  42526  etransc  42575  qndenserrnbl  42587  sge0tsms  42669  el1fzopredsuc  43532