Theorem sneq 3705

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 2244	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2354	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3700	. 2 |- { A } = { x | x = A }
4		df-sn 3700	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2292	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1398   {cab 2220   {csn 3694

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-sn 3700

This theorem is referenced by:  sneqi  3706  sneqd  3707  euabsn  3766  absneu  3768  preq1  3773  tpeq3  3784  snssgOLD  3835  sneqrg  3871  sneqbg  3872  opeq1  3888  unisng  3936  exmidsssn  4320  exmidsssnc  4321  suceq  4528  snnex  4574  opeliunxp  4810  relop  4910  elimasng  5135  dmsnsnsng  5245  elxp4  5255  elxp5  5256  iotajust  5316  fconstg  5569  f1osng  5662  nfvres  5711  fsng  5855  fsn2g  5857  funopsn  5865  fnressn  5875  fressnfv  5876  funfvima3  5925  isoselem  5999  1stvalg  6349  2ndvalg  6350  2ndval2  6363  fo1st  6364  fo2nd  6365  f1stres  6366  f2ndres  6367  mpomptsx  6406  dmmpossx  6408  fmpox  6409  suppval  6450  suppsnopdc  6463  brtpos2  6495  dftpos4  6507  tpostpos  6508  eceq1  6815  fvdiagfn  6941  mapsncnv  6943  elixpsn  6983  ixpsnf1o  6984  ensn1g  7050  en1  7052  xpsneng  7086  xpcomco  7090  xpassen  7094  xpdom2  7095  phplem3  7121  phplem3g  7123  fidifsnen  7138  xpfi  7205  pm54.43  7500  cc2lem  7596  cc2  7597  exp3val  10927  fsum2dlemstep  12145  fsumcnv  12148  fisumcom2  12149  fprod2dlemstep  12333  fprodcnv  12336  fprodcom2fi  12337  pwsval  14146  lssats2  14688  lspsneq0  14700  txswaphmeolem  15311  vtxdgfifival  16412  vtxdumgrfival  16419  1loopgrvd2fi  16426  wlk1walkdom  16480  wlkres  16500  eupth2lem3lem3fi  16591