Theorem sneq 3054

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 1893	. . 3 |- (A = B -> (x = A <-> x = B))
2	1	abbidv 2008	. 2 |- (A = B -> {x | x = A} = {x | x = B})
3		df-sn 3049	. 2 |- {A} = {x | x = A}
4		df-sn 3049	. 2 |- {B} = {x | x = B}
5	2, 3, 4	3eqtr4g 1953	1 |- (A = B -> {A} = {B})

Syntax hints:   -> wi 3   = wceq 1298  {cab 1871  {csn 3044

This theorem is referenced by:  sneqi 3055  sneqd 3056  euabsn 3095  preq1 3098  tpeq3 3102  snssg 3124  opeq1 3158  unisng 3194  snexOLD 3493  opthwiener 3554  suceq 3729  suceqOLD 3730  snnex 3801  reusn 3818  reusnOLD 3819  reusni 3820  relop 4113  elimasng 4291  elinisegOLD 4295  dmsnopOLD 4368  elxp4 4379  elxp5 4380  fconstg 4604  fveq2 4681  fnressn 4812  fressnfv 4813  funfvima3 4830  isofrlem 4878  1stval 5022  2ndval 5023  2ndval2 5031  fo1st 5032  fo2nd 5033  f1stres 5034  f2ndres 5035  iotajust 5088  tfrlem10 5128  eceq2 5336  ensn1g 5484  en1 5485  xpsneng 5495  xpcomen 5498  xpassen 5500  xpdom2 5501  canth2 5548  xpmapenlem2 5591  xpmapenlem5 5594  mapunen 5596  phplem3 5604  pm54.43 5662  aceq5lem3 5899  aceq5lem4 5900  kmlem9 5935  kmlem11 5937  kmlem12 5938  cardsn 5984  snunioo 7584  expval 7813  xpnnen 8768  islp 9020  gxval 9381  dif1enOLD 10173  fixp 10180  isfillim 10298  hausfillim 10303  filmapf 10307  on1el3 10412  h1de2ctlem 11111  spansn 11115  elspansn 11122  elspansn2 11123  spansneleq 11126  h1datom 11138  spansnj 11227  spansncv 11233  superpos 11926  sumdmdlem2 11991  bnj148 12481  bnj1313 13494  bnj1319 13495  bnj1332 13499  bnj1373 13506  sneqrg 13822  predeq3 13883  altopeq1 14087  altopeq2 14088  fatesg 14293  moec 14351  snelpwg 14415  nZdef 14527  valcurfn1 14552  osneisi 14875  plimfil 14940  limvinlv 14941  dualalg 15131  valtar 15260  locfinnei 15512  neibastop3 15524  ist1-2 15542  ist1-3 15543  t1sncld 15545  fimax 15746  inficl 15757  frfi 15771  tlmbr 15904  ismrer1 16024  atompoint 17224  watomval 17393  trnset 17405

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-sn 3049

Copyright terms: Public domain