Theorem sneq 3538

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 2149	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2257	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3533	. 2 |- { A } = { x | x = A }
4		df-sn 3533	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2197	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1331   {cab 2125   {csn 3527

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-sn 3533

This theorem is referenced by:  sneqi  3539  sneqd  3540  euabsn  3593  absneu  3595  preq1  3600  tpeq3  3611  snssg  3656  sneqrg  3689  sneqbg  3690  opeq1  3705  unisng  3753  exmidsssn  4125  exmidsssnc  4126  suceq  4324  snnex  4369  opeliunxp  4594  relop  4689  elimasng  4907  dmsnsnsng  5016  elxp4  5026  elxp5  5027  iotajust  5087  fconstg  5319  f1osng  5408  nfvres  5454  fsng  5593  fnressn  5606  fressnfv  5607  funfvima3  5651  isoselem  5721  1stvalg  6040  2ndvalg  6041  2ndval2  6054  fo1st  6055  fo2nd  6056  f1stres  6057  f2ndres  6058  mpomptsx  6095  dmmpossx  6097  fmpox  6098  brtpos2  6148  dftpos4  6160  tpostpos  6161  eceq1  6464  fvdiagfn  6587  mapsncnv  6589  elixpsn  6629  ixpsnf1o  6630  ensn1g  6691  en1  6693  xpsneng  6716  xpcomco  6720  xpassen  6724  xpdom2  6725  phplem3  6748  phplem3g  6750  fidifsnen  6764  xpfi  6818  pm54.43  7046  exp3val  10295  fsum2dlemstep  11203  fsumcnv  11206  fisumcom2  11207  txswaphmeolem  12489