Theorem sneq 3969

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 2482	. . 3 |- ( A = B -> ( x = A <-> x = B ) )
2	1	abbidv 2589	. 2 |- ( A = B -> { x | x = A } = { x | x = B } )
3		df-sn 3960	. 2 |- { A } = { x | x = A }
4		df-sn 3960	. 2 |- { B } = { x | x = B }
5	2, 3, 4	3eqtr4g 2530	1 |- ( A = B -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1452   {cab 2457   {csn 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-sn 3960

This theorem is referenced by:  sneqi  3970  sneqd  3971  euabsn  4035  absneu  4037  preq1  4042  tpeq3  4053  snssg  4096  sneqrg  4133  sneqbg  4134  opeq1  4158  unisng  4206  opthwiener  4703  otiunsndisj  4707  opeliunxp  4891  relop  4990  elimasng  5200  inisegn0  5206  xpdifid  5271  dmsnsnsn  5321  predeq123  5388  suceq  5495  iotajust  5552  fconstg  5783  f1osng  5867  opabiotafun  5941  fvn0ssdmfun  6028  fsng  6079  fsn2g  6080  fnressn  6092  fressnfv  6094  funfvima3  6160  f12dfv  6190  f13dfv  6191  isofrlem  6249  isoselem  6250  snnex  6616  elxp4  6756  elxp5  6757  1stval  6814  2ndval  6815  2ndval2  6830  fo1st  6832  fo2nd  6833  f1stres  6834  f2ndres  6835  mpt2mptsx  6875  dmmpt2ssx  6877  fmpt2x  6878  ovmptss  6896  fparlem3  6917  fparlem4  6918  suppval  6935  suppsnop  6947  ressuppssdif  6955  brtpos2  6997  dftpos4  7010  tpostpos  7011  eceq1  7417  fvdiagfn  7534  mapsncnv  7536  elixpsn  7579  ixpsnf1o  7580  ensn1g  7652  en1  7654  difsnen  7672  xpsneng  7675  xpcomco  7680  xpassen  7684  xpdom2  7685  canth2  7743  phplem3  7771  xpfi  7860  marypha2lem2  7968  cardsn  8421  pm54.43  8452  dfac5lem3  8574  dfac5lem4  8575  kmlem9  8606  kmlem11  8608  kmlem12  8609  ackbij1lem8  8675  r1om  8692  fictb  8693  hsmexlem4  8877  axcc2lem  8884  axcc2  8885  axdc3lem4  8901  fpwwe2cbv  9073  fpwwe2lem3  9076  fpwwecbv  9087  canth4  9090  fsum2dlem  13908  fsumcnv  13911  fsumcom2  13912  ackbijnn  13963  fprod2dlem  14111  fprodcnv  14114  fprodcom2  14115  lcmfunsnlem1  14689  lcmfunsnlem2lem1  14690  lcmfunsnlem2lem2  14691  lcmfunsnlem2  14692  lcmfunsn  14696  vdwlem1  15010  vdwlem12  15021  vdwlem13  15022  vdwnn  15027  0ram  15057  ramz2  15061  pwsval  15462  xpsfval  15551  xpsval  15556  symg2bas  17117  symgfixelsi  17154  pmtrfv  17171  pmtrprfval  17206  sylow2a  17349  efgrelexlema  17477  gsum2dlem2  17681  gsum2d2  17684  gsumcom2  17685  dprdcntz  17718  dprddisj  17719  dprd2dlem2  17751  dprd2dlem1  17752  dprd2da  17753  ablfac1eu  17784  ablfaclem3  17798  lssats2  18301  lspsneq0  18313  lbsind  18381  lspsneq  18423  lspdisj2  18428  lspsnsubn0  18441  lspprat  18454  islbs2  18455  lbsextlem4  18462  lbsextg  18463  lpi0  18548  lpi1  18549  psrvsca  18692  evlssca  18822  mpfind  18836  coe1fv  18876  coe1tm  18943  pf1ind  19020  frlmlbs  19432  lindfind  19451  lindsind  19452  lindfrn  19456  submaval  19683  mdetunilem3  19716  mdetunilem4  19717  mdetunilem9  19722  islp  20233  perfi  20248  t1sncld  20419  bwth  20502  dis2ndc  20552  nllyi  20567  dissnlocfin  20621  ptbasfi  20673  txkgen  20744  xkofvcn  20776  xkoinjcn  20779  qtopeu  20808  txswaphmeolem  20896  pt1hmeo  20898  elflim2  21057  cnextfvval  21158  cnextcn  21160  cnextfres1  21161  cnextfres  21162  tsmsxplem1  21245  tsmsxplem2  21246  ucncn  21378  itg11  22728  i1faddlem  22730  i1fmullem  22731  itg1addlem3  22735  itg1mulc  22741  eldv  22932  ply1lpir  23215  areambl  23963  tglngval  24675  nbgraopALT  25231  nb3graprlem2  25259  cusgrarn  25266  cusgra1v  25268  cusgra2v  25269  cusgra3v  25271  cusgrares  25279  usgrasscusgra  25290  sizeusglecusglem1  25291  uvtxel  25296  cusgrauvtxb  25303  vdgrval  25703  frgraunss  25802  frgra1v  25805  frgra2v  25806  frgra3v  25809  1vwmgra  25810  3vfriswmgra  25812  3cyclfrgrarn1  25819  n4cyclfrgra  25825  frgrancvvdeqlem4  25840  frgrawopreglem4  25854  frgraregorufr0  25859  2spotiundisj  25869  gxval  26067  h1de2ctlem  27289  spansn  27293  elspansn  27300  elspansn2  27301  spansneleq  27304  h1datom  27316  spansnj  27381  spansncv  27387  superpos  28088  sumdmdlem2  28153  aciunf1lem  28339  dfcnv2  28354  gsummpt2co  28617  locfinreflem  28741  esum2dlem  28987  sibfima  29244  sibfof  29246  bnj1373  29911  bnj1489  29937  cvmscbv  30053  cvmsdisj  30065  cvmsss2  30069  cvmliftlem15  30093  cvmlift2lem11  30108  cvmlift2lem12  30109  cvmlift2lem13  30110  mvtinf  30265  eldm3  30473  elima4  30492  fvsingle  30758  snelsingles  30760  dfiota3  30761  brapply  30776  funpartlem  30780  altopeq12  30800  ranksng  31005  neibastop3  31089  tailval  31100  filnetlem4  31108  f1omptsnlem  31808  f1omptsn  31809  mptsnun  31811  dissneqlem  31812  dissneq  31813  poimirlem4  32008  poimirlem25  32029  poimirlem26  32030  poimirlem27  32031  poimirlem31  32035  poimirlem32  32036  heiborlem3  32209  ismrer1  32234  lshpnel2N  32622  lsatlspsn2  32629  lsatlspsn  32630  lsatspn0  32637  lkrscss  32735  lfl1dim  32758  lfl1dim2N  32759  ldualvs  32774  atpointN  33379  watvalN  33629  trnsetN  33793  dih1dimatlem  34968  dihatexv  34977  dihjat1lem  35067  dihjat1  35068  lcfl7N  35140  lcfl8  35141  lcfl9a  35144  lcfrlem8  35188  lcfrlem9  35189  lcf1o  35190  mapdval2N  35269  mapdval4N  35271  mapdspex  35307  mapdn0  35308  mapdpglem23  35333  mapdpg  35345  mapdindp1  35359  mapdheq  35367  hvmapval  35399  mapdh9a  35429  hdmap1eq  35441  hdmap1cbv  35442  hdmapval  35470  hdmap10  35482  hdmaplkr  35555  mzpclval  35638  mzpcl1  35642  wopprc  35956  dnnumch3lem  35975  aomclem8  35990  mendvsca  36128  cytpval  36157  dvconstbi  36753  wessf1ornlem  37530  dvmptfprodlem  37916  fourierdlem32  38114  fourierdlem33  38115  fourierdlem48  38130  fzopredsuc  38865  issn  39142  propeqop  39146  nbgrval  39570  nbgr2vtx1edg  39582  nbuhgr2vtx1edgb  39584  nbgr1vtx  39590  nb3grprlem2  39619  uvtxael  39624  uvtxael1  39632  uvtxusgrel  39640  cusgredg  39656  cplgr1v  39662  cplgr3v  39667  usgredgsscusgredg  39685  vtxdgval  39694  1loopgrvd2  39725  1wlk1walk  39838  1wlkres  39866  1wlkp1lem8  39876  crctcsh1wlkn0lem6  39993  11wlkdlem4  40028  eupth2lem3lem3  40142  usgra2pthlem1  40175  irinitoringc  40579  opeliun2xp  40622  dmmpt2ssx2  40626  lindslinindsimp2  40764  ldepspr  40774  ldepsnlinc  40809