Theorem sneq 3630

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 2203	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2311	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3625	. 2 |- { A } = { x | x = A }
4		df-sn 3625	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2251	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1364   {cab 2179   {csn 3619

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-sn 3625

This theorem is referenced by:  sneqi  3631  sneqd  3632  euabsn  3689  absneu  3691  preq1  3696  tpeq3  3707  snssgOLD  3755  sneqrg  3789  sneqbg  3790  opeq1  3805  unisng  3853  exmidsssn  4232  exmidsssnc  4233  suceq  4434  snnex  4480  opeliunxp  4715  relop  4813  elimasng  5034  dmsnsnsng  5144  elxp4  5154  elxp5  5155  iotajust  5215  fconstg  5451  f1osng  5542  nfvres  5589  fsng  5732  fnressn  5745  fressnfv  5746  funfvima3  5793  isoselem  5864  1stvalg  6197  2ndvalg  6198  2ndval2  6211  fo1st  6212  fo2nd  6213  f1stres  6214  f2ndres  6215  mpomptsx  6252  dmmpossx  6254  fmpox  6255  brtpos2  6306  dftpos4  6318  tpostpos  6319  eceq1  6624  fvdiagfn  6749  mapsncnv  6751  elixpsn  6791  ixpsnf1o  6792  ensn1g  6853  en1  6855  xpsneng  6878  xpcomco  6882  xpassen  6886  xpdom2  6887  phplem3  6912  phplem3g  6914  fidifsnen  6928  xpfi  6988  pm54.43  7252  cc2lem  7328  cc2  7329  exp3val  10615  fsum2dlemstep  11580  fsumcnv  11583  fisumcom2  11584  fprod2dlemstep  11768  fprodcnv  11771  fprodcom2fi  11772  lssats2  13913  lspsneq0  13925  txswaphmeolem  14499