Theorem sneq 3716

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

Syntax hints:   -> wi 4   = wceq 1402   {cab 2224   {csn 3705

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 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 theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-sn 3711

This theorem is referenced by:  sneqi  3717  sneqd  3718  euabsn  3777  absneu  3779  preq1  3784  tpeq3  3795  snssgOLD  3846  sneqrg  3882  sneqbg  3883  opeq1  3899  unisng  3947  exmidsssn  4334  exmidsssnc  4335  suceq  4542  snnex  4589  opeliunxp  4825  relop  4925  elimasng  5150  dmsnsnsng  5260  elxp4  5270  elxp5  5271  iotajust  5331  fconstg  5584  f1osng  5677  nfvres  5726  fsng  5872  fsn2g  5874  funopsn  5882  fnressn  5892  fressnfv  5893  funfvima3  5942  isoselem  6016  1stvalg  6366  2ndvalg  6367  2ndval2  6380  fo1st  6381  fo2nd  6382  f1stres  6383  f2ndres  6384  mpomptsx  6423  dmmpossx  6425  fmpox  6426  suppval  6467  suppsnopdc  6480  brtpos2  6512  dftpos4  6524  tpostpos  6525  eceq1  6832  fvdiagfn  6965  mapsncnv  6967  elixpsn  7007  ixpsnf1o  7008  ensn1g  7074  en1  7076  xpsneng  7110  xpcomco  7114  xpassen  7118  xpdom2  7119  phplem3  7145  phplem3g  7147  fidifsnen  7162  xpfi  7229  pm54.43  7526  cc2lem  7622  cc2  7623  exp3val  10956  fsum2dlemstep  12179  fsumcnv  12182  fisumcom2  12183  fprod2dlemstep  12367  fprodcnv  12370  fprodcom2fi  12371  pwsval  14181  lssats2  14723  lspsneq0  14735  txswaphmeolem  15344  vtxdgfifival  16446  vtxdumgrfival  16453  1loopgrvd2fi  16460  wlk1walkdom  16514  wlkres  16534  eupth2lem3lem3fi  16625