Theorem sneq 4020

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 2456	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2577	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 4011	. 2 |- { A } = { x | x = A }
4		df-sn 4011	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2507	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1381   {cab 2426   {csn 4010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-sn 4011

This theorem is referenced by:  sneqi  4021  sneqd  4022  euabsn  4083  absneu  4085  preq1  4090  tpeq3  4101  snssg  4144  sneqrg  4180  sneqbg  4181  opeq1  4198  unisng  4246  opthwiener  4735  otiunsndisj  4739  suceq  4929  opeliunxp  5037  relop  5139  elimasng  5349  xpdifid  5421  dmsnsnsn  5472  iotajust  5536  fconstg  5758  f1osng  5840  opabiotafun  5915  fvn0ssdmfun  6003  fsng  6051  fnressn  6064  fressnfv  6066  funfvima3  6130  f12dfv  6160  f13dfv  6161  isofrlem  6217  isoselem  6218  snnex  6587  elxp4  6725  elxp5  6726  1stval  6783  2ndval  6784  2ndval2  6799  fo1st  6801  fo2nd  6802  f1stres  6803  f2ndres  6804  mpt2mptsx  6844  dmmpt2ssx  6846  fmpt2x  6847  ovmptss  6862  fparlem3  6883  fparlem4  6884  suppval  6901  suppsnop  6913  ressuppssdif  6919  brtpos2  6959  dftpos4  6972  tpostpos  6973  eceq1  7345  fvdiagfn  7461  mapsncnv  7463  elixpsn  7506  ixpsnf1o  7507  ensn1g  7578  en1  7580  difsnen  7597  xpsneng  7600  xpcomco  7605  xpassen  7609  xpdom2  7610  canth2  7668  phplem3  7696  xpfi  7789  marypha2lem2  7894  cardsn  8348  pm54.43  8379  dfac5lem3  8504  dfac5lem4  8505  kmlem9  8536  kmlem11  8538  kmlem12  8539  ackbij1lem8  8605  r1om  8622  fictb  8623  hsmexlem4  8807  axcc2lem  8814  axcc2  8815  axdc3lem4  8831  fpwwe2cbv  9006  fpwwe2lem3  9009  fpwwecbv  9020  canth4  9023  fsum2dlem  13559  fsumcnv  13562  fsumcom2  13563  ackbijnn  13614  xpnnenOLD  13815  vdwlem1  14371  vdwlem12  14382  vdwlem13  14383  vdwnn  14388  0ram  14410  ramz2  14414  pwsval  14755  xpsfval  14836  xpsval  14841  symg2bas  16292  symgfixelsi  16329  pmtrfv  16346  pmtrprfval  16381  sylow2a  16508  efgrelexlema  16636  gsum2dlem2  16867  gsum2dOLD  16869  gsum2d2  16871  gsumcom2  16872  dprdcntz  16910  dprddisj  16911  dprd2dlem2  16957  dprd2dlem1  16958  dprd2da  16959  ablfac1eu  16992  ablfaclem3  17006  lssats2  17514  lspsneq0  17526  lbsind  17594  lspsneq  17636  lspdisj2  17641  lspsnsubn0  17654  lspprat  17667  islbs2  17668  lbsextlem4  17675  lbsextg  17676  lpi0  17763  lpi1  17764  psrvsca  17912  evlssca  18059  mpfind  18073  coe1fv  18113  coe1tm  18182  pf1ind  18259  frlmlbs  18698  lindfind  18718  lindsind  18719  lindfrn  18723  submaval  18950  mdetunilem3  18983  mdetunilem4  18984  mdetunilem9  18989  islp  19507  perfi  19522  t1sncld  19693  bwth  19776  dis2ndc  19827  nllyi  19842  dissnlocfin  19896  ptbasfi  19948  txkgen  20019  xkofvcn  20051  xkoinjcn  20054  qtopeu  20083  txswaphmeolem  20171  pt1hmeo  20173  elflim2  20331  cnextfvval  20431  cnextcn  20433  cnextfres  20434  tsmsxplem1  20521  tsmsxplem2  20522  ucncn  20654  itg11  21964  i1faddlem  21966  i1fmullem  21967  itg1addlem3  21971  itg1mulc  21977  eldv  22168  ply1lpir  22445  areambl  23153  tglngval  23803  nbgraopALT  24289  nb3graprlem2  24317  cusgrarn  24324  cusgra1v  24326  cusgra2v  24327  cusgra3v  24329  cusgrares  24337  usgrasscusgra  24348  sizeusglecusglem1  24349  uvtxel  24354  cusgrauvtxb  24361  vdgrval  24761  frgraunss  24860  frgra1v  24863  frgra2v  24864  frgra3v  24867  1vwmgra  24868  3vfriswmgra  24870  3cyclfrgrarn1  24877  n4cyclfrgra  24883  frgrancvvdeqlem4  24898  frgrawopreglem4  24912  frgraregorufr0  24917  2spotiundisj  24927  gxval  25125  h1de2ctlem  26338  spansn  26342  elspansn  26349  elspansn2  26350  spansneleq  26353  h1datom  26365  spansnj  26430  spansncv  26436  superpos  27138  sumdmdlem2  27203  dfcnv2  27382  locfinreflem  27709  sibfima  28146  sibfof  28148  cvmscbv  28569  cvmsdisj  28581  cvmsss2  28585  cvmliftlem15  28609  cvmlift2lem11  28624  cvmlift2lem12  28625  cvmlift2lem13  28626  mvtinf  28781  fprod2dlem  29078  fprodcnv  29081  fprodcom2  29082  eldm3  29159  elima4  29177  predeq123  29213  fvsingle  29538  snelsingles  29540  dfiota3  29541  brapply  29556  funpartlem  29560  altopeq12  29580  ranksng  29792  neibastop3  30148  tailval  30159  filnetlem4  30167  heiborlem3  30277  ismrer1  30302  mzpclval  30625  mzpcl1  30629  wopprc  30940  inisegn0  30957  dnnumch3lem  30960  aomclem8  30975  mapfien2OLD  31010  mendvsca  31109  cytpval  31138  dvconstbi  31208  fourierdlem32  31806  fourierdlem33  31807  fourierdlem48  31822  usgra2pthlem1  32187  opeliun2xp  32630  dmmpt2ssx2  32634  lindslinindsimp2  32774  ldepspr  32784  ldepsnlinc  32819  bnj1373  33793  bnj1489  33819  lshpnel2N  34412  lsatlspsn2  34419  lsatlspsn  34420  lsatspn0  34427  lkrscss  34525  lfl1dim  34548  lfl1dim2N  34549  ldualvs  34564  atpointN  35169  watvalN  35419  trnsetN  35583  dih1dimatlem  36758  dihatexv  36767  dihjat1lem  36857  dihjat1  36858  lcfl7N  36930  lcfl8  36931  lcfl9a  36934  lcfrlem8  36978  lcfrlem9  36979  lcf1o  36980  mapdval2N  37059  mapdval4N  37061  mapdspex  37097  mapdn0  37098  mapdpglem23  37123  mapdpg  37135  mapdindp1  37149  mapdheq  37157  hvmapval  37189  mapdh9a  37219  hdmap1eq  37231  hdmap1cbv  37232  hdmapval  37260  hdmap10  37272  hdmaplkr  37345