Theorem sneq 3461

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 2098	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2206	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3456	. 2 |- { A } = { x | x = A }
4		df-sn 3456	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2146	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1290   {cab 2075   {csn 3450

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-sn 3456

This theorem is referenced by:  sneqi  3462  sneqd  3463  euabsn  3516  absneu  3518  preq1  3523  tpeq3  3534  snssg  3579  sneqrg  3612  sneqbg  3613  opeq1  3628  unisng  3676  exmidsssn  4040  suceq  4238  snnex  4283  opeliunxp  4506  relop  4599  elimasng  4813  dmsnsnsng  4921  elxp4  4931  elxp5  4932  iotajust  4992  fconstg  5220  f1osng  5307  nfvres  5350  fsng  5484  fnressn  5497  fressnfv  5498  funfvima3  5542  isoselem  5613  1stvalg  5927  2ndvalg  5928  2ndval2  5941  fo1st  5942  fo2nd  5943  f1stres  5944  f2ndres  5945  mpt2mptsx  5981  dmmpt2ssx  5983  fmpt2x  5984  brtpos2  6030  dftpos4  6042  tpostpos  6043  eceq1  6341  fvdiagfn  6464  mapsncnv  6466  elixpsn  6506  ixpsnf1o  6507  ensn1g  6568  en1  6570  xpsneng  6592  xpcomco  6596  xpassen  6600  xpdom2  6601  phplem3  6624  phplem3g  6626  fidifsnen  6640  xpfi  6694  pm54.43  6879  exp3val  10018  fsum2dlemstep  10889  fsumcnv  10892  fisumcom2  10893