Theorem sneq 4599

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 2775	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2829	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4590	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4590	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1570  {cab 2741  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-sn 4590

This theorem is referenced by:  sneqi  4600  sneqd  4601  euabsn  4692  absneu  4694  preq1  4699  tpeq3  4710  issn  4797  mosneq  4807  sneqbg  4808  opeq1  4838  snexgALT  5412  propeqop  5490  opthwiener  5497  otiunsndisj  5503  opeliunxp  5728  opeliun2xp  5729  relop  5836  inisegn0  6100  xpdifid  6165  xpdifcnvepel  6166  dmsnsnsn  6221  predeq123  6303  iotajust  6491  iotanul2  6509  fconstg  6765  f1osng  6863  opabiotafun  6961  fvn0ssdmfun  7069  fsng  7133  fsn2g  7134  fnressn  7155  fressnfv  7157  funfvima3  7234  f12dfv  7271  f13dfv  7272  isofrlem  7338  isoselem  7339  elxp4  7915  elxp5  7916  1stval  7984  2ndval  7985  2ndval2  8000  fo1st  8002  fo2nd  8003  f1stres  8006  f2ndres  8007  mpomptsx  8057  dmmpossx  8059  fmpox  8060  ovmptss  8084  fparlem3  8105  fparlem4  8106  xpord2pred  8137  xpord3pred  8144  suppval  8154  suppsnop  8170  ressuppssdif  8177  brtpos2  8224  dftpos4  8237  tpostpos  8238  naddcllem  8658  eceq1  8730  fvdiagfn  8885  mapsncnv  8887  elixpsn  8931  ixpsnf1o  8932  ensn1g  9015  en1  9017  difsnen  9043  xpsneng  9046  xpcomco  9051  xpassen  9055  xpdom2  9056  canth2  9114  rexdif1en  9141  cnvfi  9156  marypha2lem2  9392  cardsn  9951  pm54.43  9983  dfac5lem3  10105  dfac5lem4  10106  kmlem9  10138  kmlem11  10140  kmlem12  10141  ackbij1lem8  10205  r1om  10222  fictb  10223  hsmexlem4  10408  axcc2lem  10415  axcc2  10416  axdc3lem4  10432  fpwwe2cbv  10610  fpwwe2lem3  10613  fpwwecbv  10624  canth4  10627  s3iunsndisj  15001  fsum2dlem  15817  fsumcnv  15820  fsumcom2  15821  ackbijnn  15878  fprod2dlem  16030  fprodcnv  16033  fprodcom2  16034  lcmfunsnlem1  16690  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  lcmfunsnlem2  16693  lcmfunsn  16697  vdwlem1  17036  vdwlem12  17047  vdwlem13  17048  vdwnn  17053  0ram  17075  ramz2  17079  pwsval  17534  symg2bas  19458  symgfixelsi  19500  pmtrfv  19517  pmtrprfval  19552  sylow2a  19684  efgrelexlema  19814  gsum2dlem2  20036  gsum2d2  20039  gsumcom2  20040  dprdcntz  20075  dprddisj  20076  dprd2dlem2  20107  dprd2dlem1  20108  dprd2da  20109  ablfac1eu  20140  ablfaclem3  20154  lssats2  21121  lspsneq0  21133  lbsind  21201  lspsneq  21246  lspdisj2  21251  lspsnsubn0  21264  lspprat  21277  islbs2  21278  lbsextlem4  21285  lbsextg  21286  lpi0  21494  lpi1  21495  irinitoringc  21629  pzriprnglem13  21643  pzriprnglem14  21644  frlmlbs  21947  lindfind  21966  lindsind  21967  lindfrn  21971  psrvsca  22099  evlsvvval  22244  evlssca  22245  mpfind  22266  evlsevl  22283  coe1fv  22366  coe1tm  22434  pf1ind  22515  submaval  22738  mdetunilem3  22771  mdetunilem4  22772  mdetunilem9  22777  islp  23297  perfi  23312  t1sncld  23483  bwth  23567  dis2ndc  23617  nllyi  23632  dissnlocfin  23686  ptbasfi  23738  txkgen  23809  xkofvcn  23841  xkoinjcn  23844  qtopeu  23873  txswaphmeolem  23961  pt1hmeo  23963  elflim2  24121  cnextfvval  24222  cnextcn  24224  cnextfres1  24225  cnextfres  24226  tsmsxplem1  24310  tsmsxplem2  24311  ucncn  24441  itg11  25850  i1faddlem  25852  i1fmullem  25853  itg1addlem3  25857  itg1mulc  25863  eldv  26057  ply1lpir  26339  areambl  27123  conway  27972  cutsval  27973  cutcuts  27974  cutbday  27977  eqcuts  27978  eqcuts2  27979  cutsun12  27983  cutbdaybnd  27988  cutbdaybnd2  27989  cutbdaylt  27991  eqcuts3  27997  bday1  28007  cuteq0  28008  cuteq1  28010  madebdaylemlrcut  28092  sltsbday  28110  cofcut1  28113  cofcutr  28117  oniso  28464  bdayn0p1  28562  expsval  28618  pw2cut2  28655  tglngval  28820  edglnl  29493  nbgrval  29686  nbgr2vtx1edg  29700  nbuhgr2vtx1edgb  29702  nbgr1vtx  29708  nb3grprlem2  29731  uvtxel  29738  uvtxel1  29746  uvtxusgrel  29753  cusgredg  29774  cplgr1v  29780  cplgr3v  29785  usgredgsscusgredg  29809  vtxdgval  29818  1loopgrvd2  29853  wlk1walk  29988  wlkres  30018  wlkp1lem8  30028  usgr2pthlem  30112  crctcshwlkn0lem6  30164  2wspiundisj  30315  clwwlknon1  30448  1wlkdlem4  30491  eupth2lem3lem3  30581  frcond1  30617  frgr1v  30622  nfrgr2v  30623  frgr3v  30626  1vwmgr  30627  3vfriswmgr  30629  3cyclfrgrrn1  30636  n4cyclfrgr  30642  frgrwopreglem4a  30661  h1de2ctlem  31907  spansn  31911  elspansn  31918  elspansn2  31919  spansneleq  31922  h1datom  31934  spansnj  31999  spansncv  32005  superpos  32706  sumdmdlem2  32771  aciunf1lem  33007  fnpreimac  33015  dfcnv2  33020  pwrssmgc  33320  gsummpt2co  33368  gsumpart  33383  gsumwrd2dccatlem  33397  gsumwrd2dccat  33398  0nellinds  33685  lindssn  33691  lsmsnidl  33710  nsgmgclem  33720  nsgmgc  33721  nsgqusf1olem1  33722  nsgqusf1olem2  33723  nsgqusf1olem3  33724  pidlnzb  33730  elrspunidl  33736  extvfval  33922  esplyfval1  33963  esplyfvaln  33964  lbslsat  34006  lindsunlem  34014  extdgval  34043  fldextrspunlsplem  34063  locfinreflem  34230  esum2dlem  34482  sibfima  34728  sibfof  34730  bnj1373  35418  bnj1489  35444  funen1cnv  35477  fineqvac  35529  onvfowev  35600  cplgredgex  35613  pfxwlk  35616  revwlk  35617  loop1cycl  35629  cvmscbv  35750  cvmsdisj  35762  cvmsss2  35766  cvmliftlem15  35790  cvmlift2lem11  35805  cvmlift2lem12  35806  cvmlift2lem13  35807  satffunlem1lem1  35894  satffunlem2lem1  35896  mvtinf  36047  eldm3  36253  elima4  36268  fvsingle  36410  snelsingles  36412  dfiota3  36413  brapply  36428  funpartlem  36434  altopeq12  36454  ranksng  36659  neibastop3  36873  tailval  36884  filnetlem4  36892  ttcid  37003  mh-inf3sn  37053  mh-infprim2bi  37058  mh-infprim3bi  37059  bj-snexg  37670  bj-restsnss  37725  bj-restsnss2  37726  f1omptsnlem  37982  f1omptsn  37983  mptsnun  37985  dissneqlem  37986  dissneq  37987  fvineqsnf1  38056  lindsadd  38264  lindsenlbs  38266  poimirlem4  38275  poimirlem25  38296  poimirlem26  38297  poimirlem27  38298  poimirlem31  38302  poimirlem32  38303  heiborlem3  38464  ismrer1  38489  lshpnel2N  39759  lsatlspsn2  39766  lsatlspsn  39767  lsatspn0  39774  lkrscss  39872  lfl1dim  39895  lfl1dim2N  39896  ldualvs  39911  atpointN  40517  watvalN  40767  trnsetN  40930  dih1dimatlem  42103  dihatexv  42112  dihjat1lem  42202  dihjat1  42203  lcfl7N  42275  lcfl8  42276  lcfl9a  42279  lcfrlem8  42323  lcfrlem9  42324  lcf1o  42325  mapdval2N  42404  mapdval4N  42406  mapdspex  42442  mapdn0  42443  mapdpglem23  42468  mapdpg  42480  mapdindp1  42494  mapdheq  42502  hvmapval  42534  mapdh9a  42563  hdmap1eq  42575  hdmap1cbv  42576  hdmapval  42602  hdmap10  42614  hdmaplkr  42687  sn-iotalem  42992  0prjspnrel  43359  mzpclval  43456  mzpcl1  43460  wopprc  43757  dnnumch3lem  43773  aomclem8  43788  mendvsca  43914  cytpval  43929  snen1g  44250  k0004lem3  44875  dvconstbi  45044  relpfrlem  45662  permaxinf2lem  45721  wessf1ornlem  45903  dvmptfprodlem  46658  fourierdlem32  46853  fourierdlem33  46854  fourierdlem48  46868  funressnmo  47783  aiotajust  47821  funressndmafv2rn  47960  fzopredsuc  48061  elsprel  48224  clnbgrval  48587  dfvopnbgr2  48618  vopnbgrel  48619  dfclnbgr6  48621  dfnbgr6  48622  cycl3grtri  48712  dmmpossx2  49117  lindslinindsimp2  49243  ldepspr  49253  ldepsnlinc  49288  line  49512  rrxline  49514  dftpos5  49652  tposideq  49666  initc  49869  setc2othin  50244  functermceu  50288  idfudiag1  50303  funcsn  50319  0fucterm  50321  mndtcval  50357  mndtcbas  50359