Theorem sneq 4042

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 2472	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2593	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 4033	. 2 |- { A } = { x | x = A }
4		df-sn 4033	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2523	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1395   {cab 2442   {csn 4032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-sn 4033

This theorem is referenced by:  sneqi  4043  sneqd  4044  euabsn  4104  absneu  4106  preq1  4111  tpeq3  4122  snssg  4165  sneqrg  4201  sneqbg  4202  opeq1  4219  unisng  4267  opthwiener  4758  otiunsndisj  4762  suceq  4952  opeliunxp  5060  relop  5163  elimasng  5373  xpdifid  5442  dmsnsnsn  5492  iotajust  5556  fconstg  5778  f1osng  5860  opabiotafun  5934  fvn0ssdmfun  6023  fsng  6071  fnressn  6084  fressnfv  6086  funfvima3  6150  f12dfv  6180  f13dfv  6181  isofrlem  6237  isoselem  6238  snnex  6605  elxp4  6743  elxp5  6744  1stval  6801  2ndval  6802  2ndval2  6817  fo1st  6819  fo2nd  6820  f1stres  6821  f2ndres  6822  mpt2mptsx  6862  dmmpt2ssx  6864  fmpt2x  6865  ovmptss  6880  fparlem3  6901  fparlem4  6902  suppval  6919  suppsnop  6931  ressuppssdif  6939  brtpos2  6979  dftpos4  6992  tpostpos  6993  eceq1  7365  fvdiagfn  7482  mapsncnv  7484  elixpsn  7527  ixpsnf1o  7528  ensn1g  7599  en1  7601  difsnen  7618  xpsneng  7621  xpcomco  7626  xpassen  7630  xpdom2  7631  canth2  7689  phplem3  7717  xpfi  7809  marypha2lem2  7914  cardsn  8367  pm54.43  8398  dfac5lem3  8523  dfac5lem4  8524  kmlem9  8555  kmlem11  8557  kmlem12  8558  ackbij1lem8  8624  r1om  8641  fictb  8642  hsmexlem4  8826  axcc2lem  8833  axcc2  8834  axdc3lem4  8850  fpwwe2cbv  9025  fpwwe2lem3  9028  fpwwecbv  9039  canth4  9042  fsum2dlem  13597  fsumcnv  13600  fsumcom2  13601  ackbijnn  13652  fprod2dlem  13796  fprodcnv  13799  fprodcom2  13800  xpnnenOLD  13955  vdwlem1  14511  vdwlem12  14522  vdwlem13  14523  vdwnn  14528  0ram  14550  ramz2  14554  pwsval  14903  xpsfval  14984  xpsval  14989  symg2bas  16550  symgfixelsi  16587  pmtrfv  16604  pmtrprfval  16639  sylow2a  16766  efgrelexlema  16894  gsum2dlem2  17125  gsum2dOLD  17127  gsum2d2  17129  gsumcom2  17130  dprdcntz  17168  dprddisj  17169  dprd2dlem2  17216  dprd2dlem1  17217  dprd2da  17218  ablfac1eu  17251  ablfaclem3  17265  lssats2  17773  lspsneq0  17785  lbsind  17853  lspsneq  17895  lspdisj2  17900  lspsnsubn0  17913  lspprat  17926  islbs2  17927  lbsextlem4  17934  lbsextg  17935  lpi0  18022  lpi1  18023  psrvsca  18171  evlssca  18318  mpfind  18332  coe1fv  18372  coe1tm  18441  pf1ind  18518  frlmlbs  18958  lindfind  18978  lindsind  18979  lindfrn  18983  submaval  19210  mdetunilem3  19243  mdetunilem4  19244  mdetunilem9  19249  islp  19768  perfi  19783  t1sncld  19954  bwth  20037  dis2ndc  20087  nllyi  20102  dissnlocfin  20156  ptbasfi  20208  txkgen  20279  xkofvcn  20311  xkoinjcn  20314  qtopeu  20343  txswaphmeolem  20431  pt1hmeo  20433  elflim2  20591  cnextfvval  20691  cnextcn  20693  cnextfres  20694  tsmsxplem1  20781  tsmsxplem2  20782  ucncn  20914  itg11  22224  i1faddlem  22226  i1fmullem  22227  itg1addlem3  22231  itg1mulc  22237  eldv  22428  ply1lpir  22705  areambl  23414  tglngval  24064  nbgraopALT  24551  nb3graprlem2  24579  cusgrarn  24586  cusgra1v  24588  cusgra2v  24589  cusgra3v  24591  cusgrares  24599  usgrasscusgra  24610  sizeusglecusglem1  24611  uvtxel  24616  cusgrauvtxb  24623  vdgrval  25023  frgraunss  25122  frgra1v  25125  frgra2v  25126  frgra3v  25129  1vwmgra  25130  3vfriswmgra  25132  3cyclfrgrarn1  25139  n4cyclfrgra  25145  frgrancvvdeqlem4  25160  frgrawopreglem4  25174  frgraregorufr0  25179  2spotiundisj  25189  gxval  25387  h1de2ctlem  26600  spansn  26604  elspansn  26611  elspansn2  26612  spansneleq  26615  h1datom  26627  spansnj  26692  spansncv  26698  superpos  27400  sumdmdlem2  27465  aciunf1lem  27656  dfcnv2  27672  gsummpt2co  27931  locfinreflem  28004  esum2dlem  28264  sibfima  28477  sibfof  28479  cvmscbv  28900  cvmsdisj  28912  cvmsss2  28916  cvmliftlem15  28940  cvmlift2lem11  28955  cvmlift2lem12  28956  cvmlift2lem13  28957  mvtinf  29112  eldm3  29409  elima4  29426  predeq123  29462  fvsingle  29775  snelsingles  29777  dfiota3  29778  brapply  29793  funpartlem  29797  altopeq12  29817  ranksng  30029  neibastop3  30385  tailval  30396  filnetlem4  30404  heiborlem3  30514  ismrer1  30539  mzpclval  30862  mzpcl1  30866  wopprc  31176  inisegn0  31193  dnnumch3lem  31196  aomclem8  31211  mapfien2OLD  31246  mendvsca  31344  cytpval  31373  dvconstbi  31443  dvmptfprodlem  31944  fourierdlem32  32124  fourierdlem33  32125  fourierdlem48  32140  usgra2pthlem1  32615  irinitoringc  33021  opeliun2xp  33066  dmmpt2ssx2  33070  lindslinindsimp2  33208  ldepspr  33218  ldepsnlinc  33253  bnj1373  34229  bnj1489  34255  lshpnel2N  34853  lsatlspsn2  34860  lsatlspsn  34861  lsatspn0  34868  lkrscss  34966  lfl1dim  34989  lfl1dim2N  34990  ldualvs  35005  atpointN  35610  watvalN  35860  trnsetN  36024  dih1dimatlem  37199  dihatexv  37208  dihjat1lem  37298  dihjat1  37299  lcfl7N  37371  lcfl8  37372  lcfl9a  37375  lcfrlem8  37419  lcfrlem9  37420  lcf1o  37421  mapdval2N  37500  mapdval4N  37502  mapdspex  37538  mapdn0  37539  mapdpglem23  37564  mapdpg  37576  mapdindp1  37590  mapdheq  37598  hvmapval  37630  mapdh9a  37660  hdmap1eq  37672  hdmap1cbv  37673  hdmapval  37701  hdmap10  37713  hdmaplkr  37786