Theorem elsng 4449

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1508   ∈ wcel 2051  {csn 4435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-sn 4436

This theorem is referenced by:  elsn  4450  elsni  4452  snidg  4467  eltpg  4493  eldifsn  4589  eldifsnneqOLD  4594  sneqrg  4640  elsucg  6093  ltxr  12325  elfzp12  12800  fprodn0f  15203  lcmfunsnlem2  15838  ramcl  16219  initoeu2lem1  17144  pmtrdifellem4  18380  logbmpt  25082  2lgslem2  25688  xrge0tsmsbi  30563  dimkerim  30684  elzrhunit  30896  esumrnmpt2  31003  plymulx  31496  bj-projval  33863  bj-snmoore  33953  reclimc  41399  itgsincmulx  41723  dirkercncflem2  41854  dirkercncflem4  41856  fourierdlem53  41909  fourierdlem58  41914  fourierdlem60  41916  fourierdlem61  41917  fourierdlem62  41918  fourierdlem76  41932  fourierdlem101  41957  elaa2  41984  etransc  42033  qndenserrnbl  42045  sge0tsms  42127  el1fzopredsuc  42965