Theorem sneq 3720

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 2248	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2358	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3715	. 2 |- { A } = { x | x = A }
4		df-sn 3715	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2296	1 |- ( A = B -> { A } = { B } )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   {cab 2224   {csn 3709

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-sn 3715

This theorem is used by:  sneqi  3721  sneqd  3722  euabsn  3781  absneu  3783  preq1  3788  tpeq3  3799  snssgOLD  3851  sneqrg  3887  sneqbg  3888  opeq1  3904  unisng  3952  exmidsssn  4339  exmidsssnc  4340  suceq  4547  snnex  4594  opeliunxp  4830  relop  4930  elimasng  5155  dmsnsnsng  5265  elxp4  5275  elxp5  5276  iotajust  5336  fconstg  5589  f1osng  5682  nfvres  5732  fsng  5881  fsn2g  5883  funopsn  5891  fnressn  5901  fressnfv  5902  funfvima3  5952  isoselem  6026  1stvalg  6376  2ndvalg  6377  2ndval2  6390  fo1st  6391  fo2nd  6392  f1stres  6393  f2ndres  6394  mpomptsx  6433  dmmpossx  6435  fmpox  6436  suppval  6477  suppsnopdc  6490  brtpos2  6522  dftpos4  6534  tpostpos  6535  eceq1  6842  fvdiagfn  6975  mapsncnv  6977  elixpsn  7017  ixpsnf1o  7018  ensn1g  7084  en1  7086  xpsneng  7120  xpcomco  7124  xpassen  7128  xpdom2  7129  phplem3  7155  phplem3g  7157  fidifsnen  7172  xpfi  7239  pm54.43  7536  cc2lem  7632  cc2  7633  exp3val  10978  fsum2dlemstep  12201  fsumcnv  12204  fisumcom2  12205  fprod2dlemstep  12389  fprodcnv  12392  fprodcom2fi  12393  pwsval  14204  lssats2  14751  lspsneq0  14763  txswaphmeolem  15421  vtxdgfifival  16532  vtxdumgrfival  16539  1loopgrvd2fi  16546  wlk1walkdom  16600  wlkres  16620  eupth2lem3lem3fi  16711