Theorem sneq 3452

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 2097	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2205	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3447	. 2 |- { A } = { x | x = A }
4		df-sn 3447	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2145	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1289   {cab 2074   {csn 3441

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-sn 3447

This theorem is referenced by:  sneqi  3453  sneqd  3454  euabsn  3507  absneu  3509  preq1  3514  tpeq3  3525  snssg  3568  sneqrg  3601  sneqbg  3602  opeq1  3617  unisng  3665  suceq  4220  snnex  4262  opeliunxp  4481  relop  4574  elimasng  4787  dmsnsnsng  4895  elxp4  4905  elxp5  4906  iotajust  4966  fconstg  5191  f1osng  5278  nfvres  5321  fsng  5454  fnressn  5467  fressnfv  5468  funfvima3  5510  isoselem  5581  1stvalg  5895  2ndvalg  5896  2ndval2  5909  fo1st  5910  fo2nd  5911  f1stres  5912  f2ndres  5913  mpt2mptsx  5949  dmmpt2ssx  5951  fmpt2x  5952  brtpos2  5998  dftpos4  6010  tpostpos  6011  eceq1  6307  fvdiagfn  6430  mapsncnv  6432  ensn1g  6494  en1  6496  xpsneng  6518  xpcomco  6522  xpassen  6526  xpdom2  6527  phplem3  6550  phplem3g  6552  fidifsnen  6566  xpfi  6619  pm54.43  6797  exp3val  9922  fsum2dlemstep  10791  fsumcnv  10794  fisumcom2  10795