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  5522  f1osng  5614  nfvres  5663  fsng  5808  funopsn  5817  fnressn  5825  fressnfv  5826  funfvima3  5873  isoselem  5944  1stvalg  6288  2ndvalg  6289  2ndval2  6302  fo1st  6303  fo2nd  6304  f1stres  6305  f2ndres  6306  mpomptsx  6343  dmmpossx  6345  fmpox  6346  brtpos2  6397  dftpos4  6409  tpostpos  6410  eceq1  6715  fvdiagfn  6840  mapsncnv  6842  elixpsn  6882  ixpsnf1o  6883  ensn1g  6949  en1  6951  xpsneng  6981  xpcomco  6985  xpassen  6989  xpdom2  6990  phplem3  7015  phplem3g  7017  fidifsnen  7032  xpfi  7094  pm54.43  7363  cc2lem  7452  cc2  7453  exp3val  10763  fsum2dlemstep  11945  fsumcnv  11948  fisumcom2  11949  fprod2dlemstep  12133  fprodcnv  12136  fprodcom2fi  12137  pwsval  13324  lssats2  14378  lspsneq0  14390  txswaphmeolem  14994  wlk1walkdom  16070