Theorem sneq 3677

Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem sneq

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2239	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2347	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3672	. 2 |- { A } = { x | x = A }
4		df-sn 3672	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2287	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1395   {cab 2215   {csn 3666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-sn 3672

This theorem is referenced by:  sneqi  3678  sneqd  3679  euabsn  3736  absneu  3738  preq1  3743  tpeq3  3754  snssgOLD  3804  sneqrg  3840  sneqbg  3841  opeq1  3857  unisng  3905  exmidsssn  4286  exmidsssnc  4287  suceq  4493  snnex  4539  opeliunxp  4774  relop  4872  elimasng  5096  dmsnsnsng  5206  elxp4  5216  elxp5  5217  iotajust  5277  fconstg  5524  f1osng  5616  nfvres  5665  fsng  5810  funopsn  5819  fnressn  5829  fressnfv  5830  funfvima3  5877  isoselem  5950  1stvalg  6294  2ndvalg  6295  2ndval2  6308  fo1st  6309  fo2nd  6310  f1stres  6311  f2ndres  6312  mpomptsx  6349  dmmpossx  6351  fmpox  6352  brtpos2  6403  dftpos4  6415  tpostpos  6416  eceq1  6723  fvdiagfn  6848  mapsncnv  6850  elixpsn  6890  ixpsnf1o  6891  ensn1g  6957  en1  6959  xpsneng  6989  xpcomco  6993  xpassen  6997  xpdom2  6998  phplem3  7023  phplem3g  7025  fidifsnen  7040  xpfi  7105  pm54.43  7374  cc2lem  7463  cc2  7464  exp3val  10775  fsum2dlemstep  11961  fsumcnv  11964  fisumcom2  11965  fprod2dlemstep  12149  fprodcnv  12152  fprodcom2fi  12153  pwsval  13340  lssats2  14394  lspsneq0  14406  txswaphmeolem  15010  vtxdgfifival  16051  vtxdumgrfival  16058  wlk1walkdom  16105  wlkres  16123