Theorem sneq 4482

Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
sneq	⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Proof of Theorem sneq

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2806	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2860	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4473	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4473	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2856	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1522  {cab 2775  {csn 4472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-sn 4473

This theorem is referenced by:  sneqi  4483  sneqd  4484  euabsn  4569  absneu  4571  preq1  4576  tpeq3  4587  issn  4670  mosneq  4680  sneqbg  4681  opeq1  4710  propeqop  5288  opthwiener  5295  otiunsndisj  5301  opeliunxp  5505  relop  5607  elimasng  5831  inisegn0  5837  xpdifid  5901  dmsnsnsn  5952  predeq123  6024  suceq  6131  iotajust  6188  fconstg  6434  f1osng  6523  opabiotafun  6611  fvn0ssdmfun  6707  fsng  6762  fsn2g  6763  fnressn  6783  fressnfv  6785  funfvima3  6863  f12dfv  6895  f13dfv  6896  isofrlem  6956  isoselem  6957  elxp4  7483  elxp5  7484  1stval  7547  2ndval  7548  2ndval2  7563  fo1st  7565  fo2nd  7566  f1stres  7569  f2ndres  7570  mpomptsx  7618  dmmpossx  7620  fmpox  7621  ovmptss  7644  fparlem3  7665  fparlem4  7666  suppval  7683  suppsnop  7695  ressuppssdif  7702  brtpos2  7749  dftpos4  7762  tpostpos  7763  eceq1  8177  fvdiagfn  8304  mapsncnv  8306  elixpsn  8349  ixpsnf1o  8350  ensn1g  8422  en1  8424  difsnen  8446  xpsneng  8449  xpcomco  8454  xpassen  8458  xpdom2  8459  canth2  8517  phplem3  8545  xpfi  8635  marypha2lem2  8746  cardsn  9244  pm54.43  9275  dfac5lem3  9397  dfac5lem4  9398  kmlem9  9430  kmlem11  9432  kmlem12  9433  ackbij1lem8  9495  r1om  9512  fictb  9513  hsmexlem4  9697  axcc2lem  9704  axcc2  9705  axdc3lem4  9721  fpwwe2cbv  9898  fpwwe2lem3  9901  fpwwecbv  9912  canth4  9915  s3iunsndisj  14162  fsum2dlem  14958  fsumcnv  14961  fsumcom2  14962  ackbijnn  15016  fprod2dlem  15167  fprodcnv  15170  fprodcom2  15171  lcmfunsnlem1  15810  lcmfunsnlem2lem1  15811  lcmfunsnlem2lem2  15812  lcmfunsnlem2  15813  lcmfunsn  15817  vdwlem1  16146  vdwlem12  16157  vdwlem13  16158  vdwnn  16163  0ram  16185  ramz2  16189  pwsval  16588  symg2bas  18257  symgfixelsi  18294  pmtrfv  18311  pmtrprfval  18346  sylow2a  18474  efgrelexlema  18602  gsum2dlem2  18811  gsum2d2  18814  gsumcom2  18815  dprdcntz  18847  dprddisj  18848  dprd2dlem2  18879  dprd2dlem1  18880  dprd2da  18881  ablfac1eu  18912  ablfaclem3  18926  lssats2  19462  lspsneq0  19474  lbsind  19542  lspsneq  19584  lspdisj2  19589  lspsnsubn0  19602  lspprat  19615  islbs2  19616  lbsextlem4  19623  lbsextg  19624  lpi0  19709  lpi1  19710  psrvsca  19859  evlssca  19989  mpfind  20003  coe1fv  20057  coe1tm  20124  pf1ind  20200  frlmlbs  20623  lindfind  20642  lindsind  20643  lindfrn  20647  submaval  20874  mdetunilem3  20907  mdetunilem4  20908  mdetunilem9  20913  islp  21432  perfi  21447  t1sncld  21618  bwth  21702  dis2ndc  21752  nllyi  21767  dissnlocfin  21821  ptbasfi  21873  txkgen  21944  xkofvcn  21976  xkoinjcn  21979  qtopeu  22008  txswaphmeolem  22096  pt1hmeo  22098  elflim2  22256  cnextfvval  22357  cnextcn  22359  cnextfres1  22360  cnextfres  22361  tsmsxplem1  22444  tsmsxplem2  22445  ucncn  22577  itg11  23975  i1faddlem  23977  i1fmullem  23978  itg1addlem3  23982  itg1mulc  23988  eldv  24179  ply1lpir  24455  areambl  25218  tglngval  26019  edglnl  26611  nbgrval  26801  nbgr2vtx1edg  26815  nbuhgr2vtx1edgb  26817  nbgr1vtx  26823  nb3grprlem2  26846  uvtxel  26853  uvtxel1  26861  uvtxusgrel  26868  cusgredg  26889  cplgr1v  26895  cplgr3v  26900  usgredgsscusgredg  26924  vtxdgval  26933  1loopgrvd2  26968  wlk1walk  27103  wlkres  27135  wlkresOLD  27137  wlkp1lem8  27147  usgr2pthlem  27231  crctcshwlkn0lem6  27280  2wspiundisj  27429  clwwlknon1  27563  1wlkdlem4  27606  eupth2lem3lem3  27697  frcond1  27737  frgr1v  27742  nfrgr2v  27743  frgr3v  27746  1vwmgr  27747  3vfriswmgr  27749  3cyclfrgrrn1  27756  n4cyclfrgr  27762  frgrwopreglem4a  27781  h1de2ctlem  29023  spansn  29027  elspansn  29034  elspansn2  29035  spansneleq  29038  h1datom  29050  spansnj  29115  spansncv  29121  superpos  29822  sumdmdlem2  29887  aciunf1lem  30097  fnpreimac  30106  dfcnv2  30112  gsummpt2co  30495  0nellinds  30583  lindssn  30585  lbslsat  30618  lindsunlem  30624  extdgval  30648  locfinreflem  30721  esum2dlem  30968  sibfima  31213  sibfof  31215  bnj1373  31916  bnj1489  31942  funen1cnv  31971  cplgredgex  31979  loop1cycl  31992  cvmscbv  32113  cvmsdisj  32125  cvmsss2  32129  cvmliftlem15  32153  cvmlift2lem11  32168  cvmlift2lem12  32169  cvmlift2lem13  32170  satffunlem1lem1  32257  satffunlem2lem1  32259  mvtinf  32410  eldm3  32605  elima4  32627  conway  32873  scutval  32874  scutcut  32875  scutbday  32876  scutun12  32880  scutbdaybnd  32884  scutbdaylt  32885  fvsingle  32990  snelsingles  32992  dfiota3  32993  brapply  33008  funpartlem  33012  altopeq12  33032  ranksng  33237  neibastop3  33319  tailval  33330  filnetlem4  33338  bj-restsnss  33973  bj-restsnss2  33974  f1omptsnlem  34148  f1omptsn  34149  mptsnun  34151  dissneqlem  34152  dissneq  34153  fvineqsnf1  34222  lindsadd  34416  lindsenlbs  34418  poimirlem4  34427  poimirlem25  34448  poimirlem26  34449  poimirlem27  34450  poimirlem31  34454  poimirlem32  34455  heiborlem3  34623  ismrer1  34648  lshpnel2N  35652  lsatlspsn2  35659  lsatlspsn  35660  lsatspn0  35667  lkrscss  35765  lfl1dim  35788  lfl1dim2N  35789  ldualvs  35804  atpointN  36410  watvalN  36660  trnsetN  36823  dih1dimatlem  37996  dihatexv  38005  dihjat1lem  38095  dihjat1  38096  lcfl7N  38168  lcfl8  38169  lcfl9a  38172  lcfrlem8  38216  lcfrlem9  38217  lcf1o  38218  mapdval2N  38297  mapdval4N  38299  mapdspex  38335  mapdn0  38336  mapdpglem23  38361  mapdpg  38373  mapdindp1  38387  mapdheq  38395  hvmapval  38427  mapdh9a  38456  hdmap1eq  38468  hdmap1cbv  38469  hdmapval  38495  hdmap10  38507  hdmaplkr  38580  0prjspnrel  38766  mzpclval  38807  mzpcl1  38811  wopprc  39112  dnnumch3lem  39131  aomclem8  39146  mendvsca  39276  cytpval  39294  snen1g  39375  k0004lem3  39984  dvconstbi  40204  wessf1ornlem  40985  dvmptfprodlem  41770  fourierdlem32  41966  fourierdlem33  41967  fourierdlem48  41981  funressnmo  42797  aiotajust  42800  funressndmafv2rn  42938  fzopredsuc  43039  elsprel  43119  irinitoringc  43818  opeliun2xp  43859  dmmpossx2  43863  lindslinindsimp2  43998  ldepspr  44008  ldepsnlinc  44043  line  44200  rrxline  44202