Theorem sneq 4590

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 2772	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2826	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4585	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4585	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2820	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

This proof depends on syntax axioms:   → wi 4   = wceq 1569  {cab 2738  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-sn 4585

This theorem is used by:  sneqi  4591  sneqd  4592  euabsn  4683  absneu  4685  preq1  4690  tpeq3  4701  issn  4786  mosneq  4796  sneqbg  4797  opeq1  4839  snexgALT  5398  propeqop  5478  opthwiener  5486  otiunsndisj  5492  opeliunxp  5717  opeliun2xp  5718  relop  5827  inisegn0  6095  xpdifid  6158  xpdifcnvepel  6159  dmsnsnsn  6221  predeq123  6305  iotajust  6493  iotanul2  6511  fconstg  6770  f1osng  6868  opabiotafun  6966  fvn0ssdmfun  7075  fsng  7139  fsn2g  7140  fnressn  7163  fressnfv  7165  funfvima3  7243  f12dfv  7282  f13dfv  7283  isofrlem  7349  isoselem  7350  elxp4  7935  elxp5  7936  1stval  8004  2ndval  8005  2ndval2  8020  fo1st  8022  fo2nd  8023  f1stres  8026  f2ndres  8027  mpomptsx  8076  dmmpossx  8078  fmpox  8079  ovmptssOLD  8106  fparlem3  8128  fparlem4  8129  xpord2pred  8165  xpord3pred  8172  suppval  8182  suppsnop  8199  ressuppssdif  8206  brtpos2  8253  dftpos4  8266  tpostpos  8267  naddcllem  8689  eceq1  8761  fvdiagfn  8923  mapsncnv  8925  elixpsn  8969  ixpsnf1o  8970  ensn1g  9053  en1  9055  funen1cnv  9060  difsnen  9082  xpsneng  9085  xpcomco  9090  xpassen  9094  xpdom2  9095  canth2  9153  rexdif1en  9180  cnvfi  9195  marypha2lem2  9432  ranksng  9878  cardsn  10054  pm54.43  10086  dfac5lem3  10208  dfac5lem4  10209  kmlem9  10241  kmlem11  10243  kmlem12  10244  ackbij1lem8  10308  hfom  10325  fictb  10326  hsmexlem4  10511  axcc2lem  10518  axcc2  10519  axdc3lem4  10535  fpwwe2cbv  10719  fpwwe2lem3  10722  fpwwecbv  10733  canth4  10736  s3iunsndisj  15127  fsum2dlem  15942  fsumcnv  15945  fsumcom2  15946  ackbijnn  16003  fprod2dlem  16153  fprodcnv  16156  fprodcom2  16157  lcmfunsnlem1  16818  lcmfunsnlem2lem1  16819  lcmfunsnlem2lem2  16820  lcmfunsnlem2  16821  lcmfunsn  16825  vdwlem1  17165  vdwlem12  17176  vdwlem13  17177  vdwnn  17182  0ram  17204  ramz2  17208  pwsval  17663  symg2bas  19613  symgfixelsi  19655  pmtrfv  19672  pmtrprfval  19707  sylow2a  19839  efgrelexlema  19969  gsum2dlem2  20191  gsum2d2  20194  gsumcom2  20195  dprdcntz  20230  dprddisj  20231  dprd2dlem2  20262  dprd2dlem1  20263  dprd2da  20264  ablfac1eu  20295  ablfaclem3  20309  lssats2  21281  lspsneq0  21293  lbsind  21361  lspsneq  21406  lspdisj2  21411  lspsnsubn0  21424  lspprat  21437  islbs2  21438  lbsextlem4  21445  lbsextg  21446  lpi0  21656  lpi1  21657  irinitoringc  21791  pzriprnglem13  21805  pzriprnglem14  21806  frlmlbs  22109  lindfind  22128  lindsind  22129  lindfrn  22133  lindsenlbs  22163  psrvsca  22263  evlsvvval  22408  evlssca  22409  mpfind  22430  evlsevl  22447  coe1fv  22530  coe1tm  22598  pf1ind  22679  submaval  22902  mdetunilem3  22935  mdetunilem4  22936  mdetunilem9  22941  islp  23464  perfi  23479  t1sncld  23650  bwth  23734  dis2ndc  23785  nllyi  23800  dissnlocfin  23854  ptbasfi  23906  txkgen  23977  xkofvcn  24009  xkoinjcn  24012  qtopeu  24041  txswaphmeolem  24129  pt1hmeo  24131  elflim2  24289  cnextfvval  24390  cnextcn  24392  cnextfres1  24393  cnextfres  24394  tsmsxplem1  24478  tsmsxplem2  24479  ucncn  24609  itg11  26018  i1faddlem  26020  i1fmullem  26021  itg1addlem3  26025  itg1mulc  26031  eldv  26224  ply1lpir  26506  areambl  27292  conway  28171  cutsval  28172  cutcuts  28173  cutbday  28176  eqcuts  28177  eqcuts2  28178  cutsun12  28182  cutbdaybnd  28187  cutbdaybnd2  28188  cutbdaylt  28190  eqcuts3  28196  bday1  28206  cuteq0  28207  cuteq1  28209  madebdaylemlrcut  28291  sltsbday  28309  cofcut1  28312  cofcutr  28316  oniso  28663  bdayn0p1  28761  expsval  28817  pw2cut2  28854  tglngval  29020  edglnl  29727  nbgrval  29923  nbgr2vtx1edg  29937  nbuhgr2vtx1edgb  29939  nbgr1vtx  29945  nb3grprlem2  29968  uvtxel  29975  uvtxel1  29983  uvtxusgrel  29990  cusgredg  30011  cplgr1v  30017  cplgr3v  30022  usgredgsscusgredg  30046  vtxdgval  30055  1loopgrvd2  30090  wlk1walk  30225  wlkres  30255  wlkp1lem8  30265  pfxwlk  30272  revwlk  30273  usgr2pthlem  30355  crctcshwlkn0lem6  30410  2wspiundisj  30561  clwwlknon1  30694  1wlkdlem4  30737  loop1cycl  30750  eupth2lem3lem3  30837  frcond1  30873  frgr1v  30878  nfrgr2v  30879  frgr3v  30882  1vwmgr  30883  3vfriswmgr  30885  3cyclfrgrrn1  30892  n4cyclfrgr  30898  frgrwopreglem4a  30917  h1de2ctlem  32163  spansn  32167  elspansn  32174  elspansn2  32175  spansneleq  32178  h1datom  32190  spansnj  32255  spansncv  32261  superpos  32962  sumdmdlem2  33027  aciunf1lem  33304  fnpreimac  33312  dfcnv2  33317  pwrssmgc  33608  gsummpt2co  33656  gsumpart  33671  gsumwrd2dccatlem  33685  gsumwrd2dccat  33686  0nellinds  33973  lindssn  33980  lsmsnidl  33999  nsgmgclem  34009  nsgmgc  34010  nsgqusf1olem1  34011  nsgqusf1olem2  34012  nsgqusf1olem3  34013  pidlnzb  34019  elrspunidl  34025  extvfval  34211  esplyfval1  34252  esplyfvaln  34253  lbslsat  34295  lindsunlem  34303  extdgval  34332  fldextrspunlsplem  34352  locfinreflem  34519  esum2dlem  34771  sibfima  35017  sibfof  35019  bnj1373  35707  bnj1489  35733  fineqvac  35841  onvfowev  35970  cplgredgex  35982  cvmscbv  36110  cvmsdisj  36122  cvmsss2  36126  cvmliftlem15  36150  cvmlift2lem11  36165  cvmlift2lem12  36166  cvmlift2lem13  36167  satffunlem1lem1  36254  satffunlem2lem1  36256  mvtinf  36407  eldm3  36619  elima4  36633  fvsingle  36775  snelsingles  36777  dfiota3  36778  brapply  36793  funpartlem  36799  altopeq12  36820  neibastop3  37243  tailval  37254  filnetlem4  37262  ttcid  37373  mh-inf3sn  37423  mh-infprim2bi  37428  mh-infprim3bi  37429  bj-snexg  38040  bj-restsnss  38097  bj-restsnss2  38098  f1omptsnlem  38353  f1omptsn  38354  mptsnun  38356  dissneqlem  38357  dissneq  38358  fvineqsnf1  38427  lindsadd  38630  poimirlem4  38636  poimirlem25  38657  poimirlem26  38658  poimirlem27  38659  poimirlem31  38663  poimirlem32  38664  heiborlem3  38841  ismrer1  38866  lshpnel2N  40136  lsatlspsn2  40143  lsatlspsn  40144  lsatspn0  40151  lkrscss  40249  lfl1dim  40272  lfl1dim2N  40273  ldualvs  40288  atpointN  40894  watvalN  41144  trnsetN  41307  dih1dimatlem  42480  dihatexv  42489  dihjat1lem  42579  dihjat1  42580  lcfl7N  42652  lcfl8  42653  lcfl9a  42656  lcfrlem8  42700  lcfrlem9  42701  lcf1o  42702  mapdval2N  42781  mapdval4N  42783  mapdspex  42819  mapdn0  42820  mapdpglem23  42845  mapdpg  42857  mapdindp1  42871  mapdheq  42879  hvmapval  42911  mapdh9a  42940  hdmap1eq  42952  hdmap1cbv  42953  hdmapval  42979  hdmap10  42991  hdmaplkr  43064  sn-iotalem  43369  0prjspnrel  43757  mzpclval  43830  mzpcl1  43834  wopprc  44131  dnnumch3lem  44147  aomclem8  44157  mendvsca  44283  cytpval  44298  snen1g  44619  k0004lem3  45243  dvconstbi  45412  relpfrlem  46037  permaxinf2lem  46096  wessf1ornlem  46294  dvmptfprodlem  47048  fourierdlem32  47243  fourierdlem33  47244  fourierdlem48  47258  funressnmo  48210  aiotajust  48248  funressndmafv2rn  48387  fzopredsuc  48488  elsprel  48651  clnbgrval  49014  dfvopnbgr2  49045  vopnbgrel  49046  dfclnbgr6  49048  dfnbgr6  49049  cycl3grtri  49139  dmmpossx2  49543  lindslinindsimp2  49669  ldepspr  49679  ldepsnlinc  49714  line  49939  rrxline  49941  dftpos5  50081  tposideq  50095  initc  50300  setc2othin  50695  functermceu  50739  idfudiag1  50754  funcsn  50773  0fucterm  50775  mndtcval  50811  mndtcbaseu  50813