Theorem sneq 3633

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 2206	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2314	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3628	. 2 |- { A } = { x | x = A }
4		df-sn 3628	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2254	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1364   {cab 2182   {csn 3622

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-sn 3628

This theorem is referenced by:  sneqi  3634  sneqd  3635  euabsn  3692  absneu  3694  preq1  3699  tpeq3  3710  snssgOLD  3758  sneqrg  3792  sneqbg  3793  opeq1  3808  unisng  3856  exmidsssn  4235  exmidsssnc  4236  suceq  4437  snnex  4483  opeliunxp  4718  relop  4816  elimasng  5037  dmsnsnsng  5147  elxp4  5157  elxp5  5158  iotajust  5218  fconstg  5454  f1osng  5545  nfvres  5592  fsng  5735  fnressn  5748  fressnfv  5749  funfvima3  5796  isoselem  5867  1stvalg  6200  2ndvalg  6201  2ndval2  6214  fo1st  6215  fo2nd  6216  f1stres  6217  f2ndres  6218  mpomptsx  6255  dmmpossx  6257  fmpox  6258  brtpos2  6309  dftpos4  6321  tpostpos  6322  eceq1  6627  fvdiagfn  6752  mapsncnv  6754  elixpsn  6794  ixpsnf1o  6795  ensn1g  6856  en1  6858  xpsneng  6881  xpcomco  6885  xpassen  6889  xpdom2  6890  phplem3  6915  phplem3g  6917  fidifsnen  6931  xpfi  6993  pm54.43  7257  cc2lem  7333  cc2  7334  exp3val  10633  fsum2dlemstep  11599  fsumcnv  11602  fisumcom2  11603  fprod2dlemstep  11787  fprodcnv  11790  fprodcom2fi  11791  lssats2  13970  lspsneq0  13982  txswaphmeolem  14556