Theorem sneq 4601

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

Syntax hints:   → wi 4   = wceq 1567  {cab 2747  {csn 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-sn 4592

This theorem is referenced by:  sneqi  4602  sneqd  4603  euabsn  4694  absneu  4696  preq1  4701  tpeq3  4712  issn  4798  mosneq  4808  sneqbg  4809  opeq1  4839  snexgALT  5410  propeqop  5488  opthwiener  5495  otiunsndisj  5501  opeliunxp  5726  opeliun2xp  5727  relop  5834  inisegn0  6098  xpdifid  6163  xpdifcnvepel  6164  dmsnsnsn  6219  predeq123  6301  iotajust  6489  iotanul2  6507  fconstg  6763  f1osng  6861  opabiotafun  6959  fvn0ssdmfun  7067  fsng  7131  fsn2g  7132  fnressn  7153  fressnfv  7155  funfvima3  7232  f12dfv  7269  f13dfv  7270  isofrlem  7336  isoselem  7337  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  10409  axcc2lem  10416  axcc2  10417  axdc3lem4  10433  fpwwe2cbv  10611  fpwwe2lem3  10614  fpwwecbv  10625  canth4  10628  s3iunsndisj  15001  fsum2dlem  15817  fsumcnv  15820  fsumcom2  15821  ackbijnn  15878  fprod2dlem  16030  fprodcnv  16033  fprodcom2  16034  lcmfunsnlem1  16691  lcmfunsnlem2lem1  16692  lcmfunsnlem2lem2  16693  lcmfunsnlem2  16694  lcmfunsn  16698  vdwlem1  17037  vdwlem12  17048  vdwlem13  17049  vdwnn  17054  0ram  17076  ramz2  17080  pwsval  17535  symg2bas  19459  symgfixelsi  19501  pmtrfv  19518  pmtrprfval  19553  sylow2a  19685  efgrelexlema  19815  gsum2dlem2  20037  gsum2d2  20040  gsumcom2  20041  dprdcntz  20076  dprddisj  20077  dprd2dlem2  20108  dprd2dlem1  20109  dprd2da  20110  ablfac1eu  20141  ablfaclem3  20155  lssats2  21095  lspsneq0  21107  lbsind  21175  lspsneq  21220  lspdisj2  21225  lspsnsubn0  21238  lspprat  21251  islbs2  21252  lbsextlem4  21259  lbsextg  21260  lpi0  21459  lpi1  21460  irinitoringc  21594  pzriprnglem13  21608  pzriprnglem14  21609  frlmlbs  21912  lindfind  21931  lindsind  21932  lindfrn  21936  psrvsca  22064  evlsvvval  22209  evlssca  22210  mpfind  22231  evlsevl  22248  coe1fv  22331  coe1tm  22399  pf1ind  22480  submaval  22703  mdetunilem3  22736  mdetunilem4  22737  mdetunilem9  22742  islp  23262  perfi  23277  t1sncld  23448  bwth  23532  dis2ndc  23582  nllyi  23597  dissnlocfin  23651  ptbasfi  23703  txkgen  23774  xkofvcn  23806  xkoinjcn  23809  qtopeu  23838  txswaphmeolem  23926  pt1hmeo  23928  elflim2  24086  cnextfvval  24187  cnextcn  24189  cnextfres1  24190  cnextfres  24191  tsmsxplem1  24275  tsmsxplem2  24276  ucncn  24406  itg11  25815  i1faddlem  25817  i1fmullem  25818  itg1addlem3  25822  itg1mulc  25828  eldv  26022  ply1lpir  26304  areambl  27085  conway  27934  cutsval  27935  cutcuts  27936  cutbday  27939  eqcuts  27940  eqcuts2  27941  cutsun12  27945  cutbdaybnd  27950  cutbdaybnd2  27951  cutbdaylt  27953  eqcuts3  27959  bday1  27969  cuteq0  27970  cuteq1  27972  madebdaylemlrcut  28054  sltsbday  28072  cofcut1  28075  cofcutr  28079  oniso  28426  bdayn0p1  28524  expsval  28580  pw2cut2  28617  tglngval  28782  edglnl  29430  nbgrval  29623  nbgr2vtx1edg  29637  nbuhgr2vtx1edgb  29639  nbgr1vtx  29645  nb3grprlem2  29668  uvtxel  29675  uvtxel1  29683  uvtxusgrel  29690  cusgredg  29711  cplgr1v  29717  cplgr3v  29722  usgredgsscusgredg  29746  vtxdgval  29755  1loopgrvd2  29790  wlk1walk  29925  wlkres  29955  wlkp1lem8  29965  usgr2pthlem  30049  crctcshwlkn0lem6  30101  2wspiundisj  30252  clwwlknon1  30385  1wlkdlem4  30428  eupth2lem3lem3  30518  frcond1  30554  frgr1v  30559  nfrgr2v  30560  frgr3v  30563  1vwmgr  30564  3vfriswmgr  30566  3cyclfrgrrn1  30573  n4cyclfrgr  30579  frgrwopreglem4a  30598  h1de2ctlem  31844  spansn  31848  elspansn  31855  elspansn2  31856  spansneleq  31859  h1datom  31871  spansnj  31936  spansncv  31942  superpos  32643  sumdmdlem2  32708  aciunf1lem  32944  fnpreimac  32952  dfcnv2  32957  pwrssmgc  33257  gsummpt2co  33305  gsumpart  33320  gsumwrd2dccatlem  33334  gsumwrd2dccat  33335  0nellinds  33624  lindssn  33631  lsmsnidl  33650  nsgmgclem  33660  nsgmgc  33661  nsgqusf1olem1  33662  nsgqusf1olem2  33663  nsgqusf1olem3  33664  pidlnzb  33670  elrspunidl  33676  extvfval  33863  esplyfval1  33904  esplyfvaln  33905  lbslsat  33947  lindsunlem  33955  extdgval  33984  fldextrspunlsplem  34004  locfinreflem  34171  esum2dlem  34423  sibfima  34669  sibfof  34671  bnj1373  35359  bnj1489  35385  funen1cnv  35416  fineqvac  35448  onvfowev  35495  cplgredgex  35508  pfxwlk  35511  revwlk  35512  loop1cycl  35524  cvmscbv  35645  cvmsdisj  35657  cvmsss2  35661  cvmliftlem15  35685  cvmlift2lem11  35700  cvmlift2lem12  35701  cvmlift2lem13  35702  satffunlem1lem1  35789  satffunlem2lem1  35791  mvtinf  35942  eldm3  36148  elima4  36163  fvsingle  36305  snelsingles  36307  dfiota3  36308  brapply  36323  funpartlem  36329  altopeq12  36349  ranksng  36554  neibastop3  36758  tailval  36769  filnetlem4  36777  ttcid  36888  mh-inf3sn  36938  mh-infprim2bi  36943  mh-infprim3bi  36944  bj-snexg  37554  bj-restsnss  37608  bj-restsnss2  37609  f1omptsnlem  37865  f1omptsn  37866  mptsnun  37868  dissneqlem  37869  dissneq  37870  fvineqsnf1  37939  lindsadd  38147  lindsenlbs  38149  poimirlem4  38158  poimirlem25  38179  poimirlem26  38180  poimirlem27  38181  poimirlem31  38185  poimirlem32  38186  heiborlem3  38347  ismrer1  38372  lshpnel2N  39644  lsatlspsn2  39651  lsatlspsn  39652  lsatspn0  39659  lkrscss  39757  lfl1dim  39780  lfl1dim2N  39781  ldualvs  39796  atpointN  40402  watvalN  40652  trnsetN  40815  dih1dimatlem  41988  dihatexv  41997  dihjat1lem  42087  dihjat1  42088  lcfl7N  42160  lcfl8  42161  lcfl9a  42164  lcfrlem8  42208  lcfrlem9  42209  lcf1o  42210  mapdval2N  42289  mapdval4N  42291  mapdspex  42327  mapdn0  42328  mapdpglem23  42353  mapdpg  42365  mapdindp1  42379  mapdheq  42387  hvmapval  42419  mapdh9a  42448  hdmap1eq  42460  hdmap1cbv  42461  hdmapval  42487  hdmap10  42499  hdmaplkr  42572  sn-iotalem  42877  0prjspnrel  43246  mzpclval  43343  mzpcl1  43347  wopprc  43644  dnnumch3lem  43660  aomclem8  43675  mendvsca  43801  cytpval  43816  snen1g  44137  k0004lem3  44762  dvconstbi  44931  relpfrlem  45549  permaxinf2lem  45608  wessf1ornlem  45790  dvmptfprodlem  46545  fourierdlem32  46740  fourierdlem33  46741  fourierdlem48  46755  funressnmo  47667  aiotajust  47705  funressndmafv2rn  47844  fzopredsuc  47945  elsprel  48108  clnbgrval  48471  dfvopnbgr2  48502  vopnbgrel  48503  dfclnbgr6  48505  dfnbgr6  48506  cycl3grtri  48596  dmmpossx2  48997  lindslinindsimp2  49123  ldepspr  49133  ldepsnlinc  49168  line  49392  rrxline  49394  dftpos5  49532  tposideq  49546  initc  49749  setc2othin  50124  functermceu  50168  idfudiag1  50183  funcsn  50199  0fucterm  50201  mndtcval  50237  mndtcbas  50239