Theorem sneq 3985

Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-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 2466	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2587	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3976	. 2 |- { A } = { x | x = A }
4		df-sn 3976	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2517	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1370   {cab 2436   {csn 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-sn 3976

This theorem is referenced by:  sneqi  3986  sneqd  3987  euabsn  4045  absneu  4047  preq1  4052  tpeq3  4063  snssg  4105  sneqrg  4140  sneqbg  4141  opeq1  4157  unisng  4205  opthwiener  4691  suceq  4882  opeliunxp  4988  relop  5088  elimasng  5293  xpdifid  5364  dmsnsnsn  5415  iotajust  5478  fconstg  5695  f1osng  5777  opabiotafun  5851  fsng  5981  fnressn  5993  fressnfv  5995  funfvima3  6053  isofrlem  6130  isoselem  6131  snnex  6482  elxp4  6622  elxp5  6623  1stval  6679  2ndval  6680  2ndval2  6695  fo1st  6696  fo2nd  6697  f1stres  6698  f2ndres  6699  mpt2mptsx  6737  dmmpt2ssx  6739  fmpt2x  6740  ovmptss  6754  fparlem3  6774  fparlem4  6775  suppval  6792  suppsnop  6804  ressuppssdif  6810  brtpos2  6851  dftpos4  6864  tpostpos  6865  eceq1  7237  fvdiagfn  7357  mapsncnv  7359  elixpsn  7402  ixpsnf1o  7403  ensn1g  7474  en1  7476  difsnen  7493  xpsneng  7496  xpcomco  7501  xpassen  7505  xpdom2  7506  canth2  7564  phplem3  7592  xpfi  7684  marypha2lem2  7787  cardsn  8240  pm54.43  8271  dfac5lem3  8396  dfac5lem4  8397  kmlem9  8428  kmlem11  8430  kmlem12  8431  ackbij1lem8  8497  r1om  8514  fictb  8515  hsmexlem4  8699  axcc2lem  8706  axcc2  8707  axdc3lem4  8723  fpwwe2cbv  8898  fpwwe2lem3  8901  fpwwecbv  8912  canth4  8915  fsum2dlem  13339  fsumcnv  13342  fsumcom2  13343  ackbijnn  13393  xpnnenOLD  13594  vdwlem1  14144  vdwlem12  14155  vdwlem13  14156  vdwnn  14161  0ram  14183  ramz2  14187  pwsval  14526  xpsfval  14607  xpsval  14612  symg2bas  16005  symgfixelsi  16042  pmtrfv  16060  pmtrprfval  16095  sylow2a  16222  efgrelexlema  16350  gsum2dlem2  16567  gsum2dOLD  16569  gsum2d2  16571  gsumcom2  16572  dprdcntz  16597  dprddisj  16598  dprd2dlem2  16644  dprd2dlem1  16645  dprd2da  16646  ablfac1eu  16679  ablfaclem3  16693  lssats2  17187  lspsneq0  17199  lbsind  17267  lspsneq  17309  lspdisj2  17314  lspsnsubn0  17327  lspprat  17340  islbs2  17341  lbsextlem4  17348  lbsextg  17349  lpi0  17435  lpi1  17436  psrvsca  17568  evlssca  17715  mpfind  17729  coe1fv  17769  coe1tm  17834  pf1ind  17898  frlmlbs  18334  lindfind  18354  lindsind  18355  lindfrn  18359  submaval  18503  mdetunilem3  18536  mdetunilem4  18537  mdetunilem9  18542  islp  18860  perfi  18875  t1sncld  19046  bwth  19129  dis2ndc  19180  nllyi  19195  ptbasfi  19270  txkgen  19341  xkofvcn  19373  xkoinjcn  19376  qtopeu  19405  txswaphmeolem  19493  pt1hmeo  19495  elflim2  19653  cnextfvval  19753  cnextcn  19755  cnextfres  19756  tsmsxplem1  19843  tsmsxplem2  19844  ucncn  19976  itg11  21285  i1faddlem  21287  i1fmullem  21288  itg1addlem3  21292  itg1mulc  21298  eldv  21489  ply1lpir  21766  areambl  22468  tglngval  23104  nb3graprlem2  23495  cusgrarn  23502  cusgra1v  23504  cusgra2v  23505  cusgra3v  23507  cusgrares  23515  usgrasscusgra  23526  sizeusglecusglem1  23527  uvtxel  23532  cusgrauvtxb  23539  vdgrval  23701  gxval  23880  h1de2ctlem  25093  spansn  25097  elspansn  25104  elspansn2  25105  spansneleq  25108  h1datom  25120  spansnj  25185  spansncv  25191  superpos  25893  sumdmdlem2  25958  dfcnv2  26128  sibfima  26858  sibfof  26860  cvmscbv  27281  cvmsdisj  27293  cvmsss2  27297  cvmliftlem15  27321  cvmlift2lem11  27336  cvmlift2lem12  27337  cvmlift2lem13  27338  fprod2dlem  27625  fprodcnv  27628  fprodcom2  27629  eldm3  27706  elima4  27724  predeq123  27760  fvsingle  28085  snelsingles  28087  dfiota3  28088  brapply  28103  funpartlem  28107  altopeq12  28127  ranksng  28339  neibastop3  28721  tailval  28732  filnetlem4  28740  heiborlem3  28850  ismrer1  28875  mzpclval  29199  mzpcl1  29203  wopprc  29517  inisegn0  29534  dnnumch3lem  29537  aomclem8  29552  mapfien2OLD  29587  mendvsca  29686  cytpval  29715  dvconstbi  29746  otiunsndisj  30270  f12dfv  30284  f13dfv  30285  usgra2pthlem1  30438  frgraunss  30725  frgra1v  30728  frgra2v  30729  frgra3v  30732  1vwmgra  30733  3vfriswmgra  30735  3cyclfrgrarn1  30742  n4cyclfrgra  30748  frgrancvvdeqlem4  30764  frgrawopreglem4  30778  frgraregorufr0  30783  2spotiundisj  30793  opeliun2xp  30858  dmmpt2ssx2  30865  lindslinindsimp2  31104  ldepspr  31114  ldepsnlinc  31157  bnj1373  32321  bnj1489  32347  lshpnel2N  32936  lsatlspsn2  32943  lsatlspsn  32944  lsatspn0  32951  lkrscss  33049  lfl1dim  33072  lfl1dim2N  33073  ldualvs  33088  atpointN  33693  watvalN  33943  trnsetN  34106  dih1dimatlem  35280  dihatexv  35289  dihjat1lem  35379  dihjat1  35380  lcfl7N  35452  lcfl8  35453  lcfl9a  35456  lcfrlem8  35500  lcfrlem9  35501  lcf1o  35502  mapdval2N  35581  mapdval4N  35583  mapdspex  35619  mapdn0  35620  mapdpglem23  35645  mapdpg  35657  mapdindp1  35671  mapdheq  35679  hvmapval  35711  mapdh9a  35741  hdmap1eq  35753  hdmap1cbv  35754  hdmapval  35782  hdmap10  35794  hdmaplkr  35867