Theorem sneq 2407

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		eqeq2 1476	. . 3 |- (A = B -> (x = A <-> x = B))
2	1	abbidv 1569	. 2 |- (A = B -> {x | x = A} = {x | x = B})
3		df-sn 2402	. 2 |- {A} = {x | x = A}
4		df-sn 2402	. 2 |- {B} = {x | x = B}
5	2, 3, 4	3eqtr4g 1523	1 |- (A = B -> {A} = {B})

Syntax hints:   -> wi 3   = wceq 953  {cab 1456  {csn 2399

This theorem is referenced by:  sneqi 2408  sneqd 2409  eusn 2436  preq1 2438  snssg 2454  opeq1 2478  unisng 2508  snex 2740  opthwiener 2796  reusn 2882  reusni 2883  suceq 3024  relop 3265  dmsnop 3317  elimasng 3411  eliniseg 3413  elxp4 3439  elxp5 3440  fconstg 3644  fveq2 3709  fnressn 3822  fressnfv 3823  funfvima3 3839  isofrlem 3886  tfrlem10 3905  1stval 4065  2ndval 4066  2ndval2 4074  fo1st 4075  fo2nd 4076  f1stres 4077  f2ndres 4078  eceq2 4262  ensn1g 4406  en1 4407  xpsneng 4416  xpcomen 4419  xpassen 4421  xpdom2 4422  canth2 4464  xpmapenlem2 4477  xpmapenlem5 4480  mapunen 4482  phplem3 4490  pm54.43 4546  aceq5lem3 4709  aceq5lem4 4710  kmlem9 4745  kmlem11 4747  kmlem12 4748  cardsn 4806  snunioo 6348  expvalt 6502  xpnnen 7441  islp 7685  h1de2ctlem 9394  spansnt 9398  elspansnt 9405  elspansn2t 9406  spansneleq 9409  spansneleqOLD 9410  h1datomt 9422  spansnjt 9509  spansncvt 9515  superpos 10189  sumdmdlem2 10253  moec 10357

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-sn 2402

Copyright terms: Public domain