Theorem sneq 3571

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 2167	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2275	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3566	. 2 |- { A } = { x | x = A }
4		df-sn 3566	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2215	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1335   {cab 2143   {csn 3560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-sn 3566

This theorem is referenced by:  sneqi  3572  sneqd  3573  euabsn  3629  absneu  3631  preq1  3636  tpeq3  3647  snssg  3692  sneqrg  3725  sneqbg  3726  opeq1  3741  unisng  3789  exmidsssn  4163  exmidsssnc  4164  suceq  4362  snnex  4408  opeliunxp  4641  relop  4736  elimasng  4954  dmsnsnsng  5063  elxp4  5073  elxp5  5074  iotajust  5134  fconstg  5366  f1osng  5455  nfvres  5501  fsng  5640  fnressn  5653  fressnfv  5654  funfvima3  5700  isoselem  5770  1stvalg  6090  2ndvalg  6091  2ndval2  6104  fo1st  6105  fo2nd  6106  f1stres  6107  f2ndres  6108  mpomptsx  6145  dmmpossx  6147  fmpox  6148  brtpos2  6198  dftpos4  6210  tpostpos  6211  eceq1  6515  fvdiagfn  6638  mapsncnv  6640  elixpsn  6680  ixpsnf1o  6681  ensn1g  6742  en1  6744  xpsneng  6767  xpcomco  6771  xpassen  6775  xpdom2  6776  phplem3  6799  phplem3g  6801  fidifsnen  6815  xpfi  6874  pm54.43  7125  cc2lem  7186  cc2  7187  exp3val  10421  fsum2dlemstep  11331  fsumcnv  11334  fisumcom2  11335  fprod2dlemstep  11519  fprodcnv  11522  fprodcom2fi  11523  txswaphmeolem  12731