Theorem sneq 3618

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 2199	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2307	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3613	. 2 |- { A } = { x | x = A }
4		df-sn 3613	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2247	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1364   {cab 2175   {csn 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-sn 3613

This theorem is referenced by:  sneqi  3619  sneqd  3620  euabsn  3677  absneu  3679  preq1  3684  tpeq3  3695  snssgOLD  3743  sneqrg  3777  sneqbg  3778  opeq1  3793  unisng  3841  exmidsssn  4220  exmidsssnc  4221  suceq  4420  snnex  4466  opeliunxp  4699  relop  4795  elimasng  5014  dmsnsnsng  5124  elxp4  5134  elxp5  5135  iotajust  5195  fconstg  5431  f1osng  5521  nfvres  5568  fsng  5710  fnressn  5723  fressnfv  5724  funfvima3  5771  isoselem  5842  1stvalg  6167  2ndvalg  6168  2ndval2  6181  fo1st  6182  fo2nd  6183  f1stres  6184  f2ndres  6185  mpomptsx  6222  dmmpossx  6224  fmpox  6225  brtpos2  6276  dftpos4  6288  tpostpos  6289  eceq1  6594  fvdiagfn  6719  mapsncnv  6721  elixpsn  6761  ixpsnf1o  6762  ensn1g  6823  en1  6825  xpsneng  6848  xpcomco  6852  xpassen  6856  xpdom2  6857  phplem3  6882  phplem3g  6884  fidifsnen  6898  xpfi  6958  pm54.43  7219  cc2lem  7295  cc2  7296  exp3val  10553  fsum2dlemstep  11474  fsumcnv  11477  fisumcom2  11478  fprod2dlemstep  11662  fprodcnv  11665  fprodcom2fi  11666  lssats2  13730  lspsneq0  13742  txswaphmeolem  14277