Theorem sneq 3543

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 2150	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2258	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3538	. 2 |- { A } = { x | x = A }
4		df-sn 3538	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2198	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1332   {cab 2126   {csn 3532

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-sn 3538

This theorem is referenced by:  sneqi  3544  sneqd  3545  euabsn  3601  absneu  3603  preq1  3608  tpeq3  3619  snssg  3664  sneqrg  3697  sneqbg  3698  opeq1  3713  unisng  3761  exmidsssn  4133  exmidsssnc  4134  suceq  4332  snnex  4377  opeliunxp  4602  relop  4697  elimasng  4915  dmsnsnsng  5024  elxp4  5034  elxp5  5035  iotajust  5095  fconstg  5327  f1osng  5416  nfvres  5462  fsng  5601  fnressn  5614  fressnfv  5615  funfvima3  5659  isoselem  5729  1stvalg  6048  2ndvalg  6049  2ndval2  6062  fo1st  6063  fo2nd  6064  f1stres  6065  f2ndres  6066  mpomptsx  6103  dmmpossx  6105  fmpox  6106  brtpos2  6156  dftpos4  6168  tpostpos  6169  eceq1  6472  fvdiagfn  6595  mapsncnv  6597  elixpsn  6637  ixpsnf1o  6638  ensn1g  6699  en1  6701  xpsneng  6724  xpcomco  6728  xpassen  6732  xpdom2  6733  phplem3  6756  phplem3g  6758  fidifsnen  6772  xpfi  6826  pm54.43  7063  cc2lem  7098  cc2  7099  exp3val  10326  fsum2dlemstep  11235  fsumcnv  11238  fisumcom2  11239  txswaphmeolem  12528