Theorem sneq 1816

Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15.

Assertion

Ref	Expression
sneq	|- (A = B -> {A} = {B})

Proof of Theorem sneq

Step	Hyp	Ref	Expression
1		cleq2 1110	. . 3 |- (A = B -> (x = A <-> x = B))
2	1	biabdv 1183	. 2 |- (A = B -> {x | x = A} = {x | x = B})
3		df-sn 1811	. 2 |- {A} = {x | x = A}
4		df-sn 1811	. 2 |- {B} = {x | x = B}
5	2, 3, 4	3eqtr4g 1147	1 |- (A = B -> {A} = {B})

Syntax hints:   -> wi 2  {cab 1090   = wceq 1091  {csn 1808

This theorem is referenced by:  sneqi 1817  sneqd 1818  snssg 1850  snex 1859  preq1 1870  opeq1 1876  eusn 1913  opthwiener 1914  unisng 1933  suceq 2288  dmsnop 2547  eliniseg 2618  elxp4 2640  elxp5 2641  fconstg 2775  fveq2 2832  fnressn 2897  fressnfv 2898  funfvima3 2906  isofrlem 2939  tfrlem10 2958  1stval 3089  2ndval 3090  fo1st 3094  fo2nd 3095  f1stres 3096  eceq2 3215  ensn1g 3330  en1 3331  en2sn 3336  snfi 3337  xpsneng 3340  xpcomen 3343  xpassen 3344  xpdom2 3345  canth2 3381  xpmapenlem2 3392  xpmapenlem5 3395  mapunen 3397  phplem4 3406  aceq5lem3 3560  aceq5lem4 3561  kmlem8 3587  kmlem10 3589  kmlem11 3590  expvalt 4677  xpnnen 4927  h1de2ctlem 5460  spansnt 5464  elspansnt 5471  elspansn2t 5472  spansneleq 5475  h1datomt 5484  spansnjt 5540  spansncvt 5543

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-sn 1811

metamath.org