Theorem sneq 3875

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 2442	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2547	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3866	. 2 |- { A } = { x | x = A }
4		df-sn 3866	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2490	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1362   {cab 2419   {csn 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-sn 3866

This theorem is referenced by:  sneqi  3876  sneqd  3877  euabsn  3935  absneu  3937  preq1  3942  tpeq3  3953  snssg  3995  sneqrg  4030  sneqbg  4031  opeq1  4047  unisng  4095  opthwiener  4581  suceq  4771  opeliunxp  4877  relop  4977  elimasng  5183  xpdifid  5254  dmsnsnsn  5305  iotajust  5368  fconstg  5585  f1osng  5667  opabiotafun  5740  fsng  5869  fnressn  5881  fressnfv  5883  funfvima3  5941  isofrlem  6018  isoselem  6019  snnex  6371  elxp4  6511  elxp5  6512  1stval  6568  2ndval  6569  2ndval2  6584  fo1st  6585  fo2nd  6586  f1stres  6587  f2ndres  6588  mpt2mptsx  6626  dmmpt2ssx  6628  fmpt2x  6629  ovmptss  6643  fparlem3  6663  fparlem4  6664  suppval  6681  suppsnop  6693  ressuppssdif  6699  brtpos2  6740  dftpos4  6753  tpostpos  6754  eceq1  7125  fvdiagfn  7245  mapsncnv  7247  elixpsn  7290  ixpsnf1o  7291  ensn1g  7362  en1  7364  difsnen  7381  xpsneng  7384  xpcomco  7389  xpassen  7393  xpdom2  7394  canth2  7452  phplem3  7480  xpfi  7571  marypha2lem2  7674  cardsn  8127  pm54.43  8158  dfac5lem3  8283  dfac5lem4  8284  kmlem9  8315  kmlem11  8317  kmlem12  8318  ackbij1lem8  8384  r1om  8401  fictb  8402  hsmexlem4  8586  axcc2lem  8593  axcc2  8594  axdc3lem4  8610  fpwwe2cbv  8785  fpwwe2lem3  8788  fpwwecbv  8799  canth4  8802  fsum2dlem  13221  fsumcnv  13224  fsumcom2  13225  ackbijnn  13274  xpnnenOLD  13475  vdwlem1  14025  vdwlem12  14036  vdwlem13  14037  vdwnn  14042  0ram  14064  ramz2  14068  pwsval  14407  xpsfval  14488  xpsval  14493  symg2bas  15883  symgfixelsi  15920  pmtrfv  15938  pmtrprfval  15973  sylow2a  16098  efgrelexlema  16226  gsum2dlem2  16436  gsum2dOLD  16438  gsum2d2  16440  gsumcom2  16441  dprdcntz  16466  dprddisj  16467  dprd2dlem2  16513  dprd2dlem1  16514  dprd2da  16515  ablfac1eu  16548  ablfaclem3  16562  lssats2  17003  lspsneq0  17015  lbsind  17083  lspsneq  17125  lspdisj2  17130  lspsnsubn0  17143  lspprat  17156  islbs2  17157  lbsextlem4  17164  lbsextg  17165  lpi0  17251  lpi1  17252  psrvsca  17396  coe1fv  17561  coe1tm  17624  frlmlbs  18067  lindfind  18087  lindsind  18088  lindfrn  18092  submaval  18234  mdetunilem3  18262  mdetunilem4  18263  mdetunilem9  18268  islp  18586  perfi  18601  t1sncld  18772  bwth  18855  dis2ndc  18906  nllyi  18921  ptbasfi  18996  txkgen  19067  xkofvcn  19099  xkoinjcn  19102  qtopeu  19131  txswaphmeolem  19219  pt1hmeo  19221  elflim2  19379  cnextfvval  19479  cnextcn  19481  cnextfres  19482  tsmsxplem1  19569  tsmsxplem2  19570  ucncn  19702  itg11  21011  i1faddlem  21013  i1fmullem  21014  itg1addlem3  21018  itg1mulc  21024  eldv  21215  evlssca  21374  mpfind  21396  pf1ind  21406  ply1lpir  21535  areambl  22237  tglngval  22864  nb3graprlem2  23183  cusgrarn  23190  cusgra1v  23192  cusgra2v  23193  cusgra3v  23195  cusgrares  23203  usgrasscusgra  23214  sizeusglecusglem1  23215  uvtxel  23220  cusgrauvtxb  23227  vdgrval  23389  gxval  23568  h1de2ctlem  24781  spansn  24785  elspansn  24792  elspansn2  24793  spansneleq  24796  h1datom  24808  spansnj  24873  spansncv  24879  superpos  25581  sumdmdlem2  25646  dfcnv2  25818  sibfima  26572  sibfof  26574  cvmscbv  26995  cvmsdisj  27007  cvmsss2  27011  cvmliftlem15  27035  cvmlift2lem11  27050  cvmlift2lem12  27051  cvmlift2lem13  27052  fprod2dlem  27338  fprodcnv  27341  fprodcom2  27342  eldm3  27419  elima4  27437  predeq123  27473  fvsingle  27798  snelsingles  27800  dfiota3  27801  brapply  27816  funpartlem  27820  altopeq12  27840  ranksng  28052  neibastop3  28427  tailval  28438  filnetlem4  28446  heiborlem3  28556  ismrer1  28581  mzpclval  28906  mzpcl1  28910  wopprc  29224  inisegn0  29241  dnnumch3lem  29244  aomclem8  29259  mapfien2OLD  29294  mendvsca  29393  cytpval  29422  dvconstbi  29453  otiunsndisj  29978  f12dfv  29992  f13dfv  29993  usgra2pthlem1  30146  frgraunss  30433  frgra1v  30436  frgra2v  30437  frgra3v  30440  1vwmgra  30441  3vfriswmgra  30443  3cyclfrgrarn1  30450  n4cyclfrgra  30456  frgrancvvdeqlem4  30472  frgrawopreglem4  30486  frgraregorufr0  30491  2spotiundisj  30501  opeliun2xp  30565  dmmpt2ssx2  30571  lindslinindsimp2  30706  ldepspr  30716  ldepsnlinc  30759  bnj1373  31723  bnj1489  31749  lshpnel2N  32203  lsatlspsn2  32210  lsatlspsn  32211  lsatspn0  32218  lkrscss  32316  lfl1dim  32339  lfl1dim2N  32340  ldualvs  32355  atpointN  32960  watvalN  33210  trnsetN  33373  dih1dimatlem  34547  dihatexv  34556  dihjat1lem  34646  dihjat1  34647  lcfl7N  34719  lcfl8  34720  lcfl9a  34723  lcfrlem8  34767  lcfrlem9  34768  lcf1o  34769  mapdval2N  34848  mapdval4N  34850  mapdspex  34886  mapdn0  34887  mapdpglem23  34912  mapdpg  34924  mapdindp1  34938  mapdheq  34946  hvmapval  34978  mapdh9a  35008  hdmap1eq  35020  hdmap1cbv  35021  hdmapval  35049  hdmap10  35061  hdmaplkr  35134