Theorem sneq 4589

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 2773	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2827	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4580	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4580	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2821	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1559  {cab 2739  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-sn 4580

This theorem is referenced by:  sneqi  4590  sneqd  4591  euabsn  4682  absneu  4684  preq1  4689  tpeq3  4700  issn  4787  mosneq  4797  sneqbg  4798  opeq1  4828  snexgALT  5395  propeqop  5473  opthwiener  5480  otiunsndisj  5486  opeliunxp  5710  opeliun2xp  5711  relop  5818  inisegn0  6083  xpdifid  6149  dmsnsnsn  6202  predeq123  6284  iotajust  6471  iotanul2  6489  fconstg  6746  f1osng  6844  opabiotafun  6942  fvn0ssdmfun  7050  fsng  7114  fsn2g  7115  fnressn  7136  fressnfv  7138  funfvima3  7215  f12dfv  7252  f13dfv  7253  isofrlem  7319  isoselem  7320  elxp4  7898  elxp5  7899  1stval  7967  2ndval  7968  2ndval2  7983  fo1st  7985  fo2nd  7986  f1stres  7989  f2ndres  7990  mpomptsx  8040  dmmpossx  8042  fmpox  8043  ovmptss  8066  fparlem3  8087  fparlem4  8088  xpord2pred  8119  xpord3pred  8126  suppval  8136  suppsnop  8152  ressuppssdif  8159  brtpos2  8206  dftpos4  8219  tpostpos  8220  naddcllem  8640  eceq1  8712  fvdiagfn  8867  mapsncnv  8869  elixpsn  8913  ixpsnf1o  8914  ensn1g  8997  en1  8999  difsnen  9025  xpsneng  9028  xpcomco  9033  xpassen  9037  xpdom2  9038  canth2  9096  rexdif1en  9123  cnvfi  9138  marypha2lem2  9376  cardsn  9921  pm54.43  9953  dfac5lem3  10075  dfac5lem4  10076  dfac5lem4OLD  10078  kmlem9  10109  kmlem11  10111  kmlem12  10112  ackbij1lem8  10176  r1om  10193  fictb  10194  hsmexlem4  10380  axcc2lem  10387  axcc2  10388  axdc3lem4  10404  fpwwe2cbv  10582  fpwwe2lem3  10585  fpwwecbv  10596  canth4  10599  s3iunsndisj  14975  fsum2dlem  15788  fsumcnv  15791  fsumcom2  15792  ackbijnn  15849  fprod2dlem  16001  fprodcnv  16004  fprodcom2  16005  lcmfunsnlem1  16662  lcmfunsnlem2lem1  16663  lcmfunsnlem2lem2  16664  lcmfunsnlem2  16665  lcmfunsn  16669  vdwlem1  17008  vdwlem12  17019  vdwlem13  17020  vdwnn  17025  0ram  17047  ramz2  17051  pwsval  17506  symg2bas  19424  symgfixelsi  19466  pmtrfv  19483  pmtrprfval  19518  sylow2a  19650  efgrelexlema  19780  gsum2dlem2  20002  gsum2d2  20005  gsumcom2  20006  dprdcntz  20041  dprddisj  20042  dprd2dlem2  20073  dprd2dlem1  20074  dprd2da  20075  ablfac1eu  20106  ablfaclem3  20120  lssats2  21055  lspsneq0  21067  lbsind  21135  lspsneq  21180  lspdisj2  21185  lspsnsubn0  21198  lspprat  21211  islbs2  21212  lbsextlem4  21219  lbsextg  21220  lpi0  21384  lpi1  21385  irinitoringc  21519  pzriprnglem13  21533  pzriprnglem14  21534  frlmlbs  21837  lindfind  21856  lindsind  21857  lindfrn  21861  psrvsca  21989  evlsvvval  22134  evlssca  22135  mpfind  22156  evlsevl  22173  coe1fv  22256  coe1tm  22324  pf1ind  22406  submaval  22629  mdetunilem3  22662  mdetunilem4  22663  mdetunilem9  22668  islp  23188  perfi  23203  t1sncld  23374  bwth  23458  dis2ndc  23508  nllyi  23523  dissnlocfin  23577  ptbasfi  23629  txkgen  23700  xkofvcn  23732  xkoinjcn  23735  qtopeu  23764  txswaphmeolem  23852  pt1hmeo  23854  elflim2  24012  cnextfvval  24113  cnextcn  24115  cnextfres1  24116  cnextfres  24117  tsmsxplem1  24201  tsmsxplem2  24202  ucncn  24332  itg11  25741  i1faddlem  25743  i1fmullem  25744  itg1addlem3  25748  itg1mulc  25754  eldv  25948  ply1lpir  26230  areambl  27011  conway  27860  cutsval  27861  cutcuts  27862  cutbday  27865  eqcuts  27866  eqcuts2  27867  cutsun12  27871  cutbdaybnd  27876  cutbdaybnd2  27877  cutbdaylt  27879  eqcuts3  27885  bday1  27895  cuteq0  27896  cuteq1  27898  madebdaylemlrcut  27980  sltsbday  27998  cofcut1  28001  cofcutr  28005  oniso  28352  bdayn0p1  28450  expsval  28506  pw2cut2  28543  tglngval  28708  edglnl  29301  nbgrval  29494  nbgr2vtx1edg  29508  nbuhgr2vtx1edgb  29510  nbgr1vtx  29516  nb3grprlem2  29539  uvtxel  29546  uvtxel1  29554  uvtxusgrel  29561  cusgredg  29582  cplgr1v  29588  cplgr3v  29593  usgredgsscusgredg  29617  vtxdgval  29626  1loopgrvd2  29661  wlk1walk  29796  wlkres  29826  wlkp1lem8  29836  usgr2pthlem  29920  crctcshwlkn0lem6  29972  2wspiundisj  30123  clwwlknon1  30256  1wlkdlem4  30299  eupth2lem3lem3  30389  frcond1  30425  frgr1v  30430  nfrgr2v  30431  frgr3v  30434  1vwmgr  30435  3vfriswmgr  30437  3cyclfrgrrn1  30444  n4cyclfrgr  30450  frgrwopreglem4a  30469  h1de2ctlem  31715  spansn  31719  elspansn  31726  elspansn2  31727  spansneleq  31730  h1datom  31742  spansnj  31807  spansncv  31813  superpos  32514  sumdmdlem2  32579  aciunf1lem  32825  fnpreimac  32833  dfcnv2  32838  pwrssmgc  33139  gsummpt2co  33189  gsumpart  33204  gsumwrd2dccatlem  33218  gsumwrd2dccat  33219  0nellinds  33517  lindssn  33525  lsmsnidl  33546  nsgmgclem  33558  nsgmgc  33559  nsgqusf1olem1  33560  nsgqusf1olem2  33561  nsgqusf1olem3  33562  pidlnzb  33569  elrspunidl  33575  extvfval  33790  esplyfval1  33831  esplyfvaln  33832  lbslsat  33874  lindsunlem  33882  extdgval  33911  fldextrspunlsplem  33931  locfinreflem  34098  esum2dlem  34350  sibfima  34596  sibfof  34598  bnj1373  35286  bnj1489  35312  funen1cnv  35343  fineqvac  35373  onvfowev  35420  cplgredgex  35432  pfxwlk  35435  revwlk  35436  loop1cycl  35448  cvmscbv  35569  cvmsdisj  35581  cvmsss2  35585  cvmliftlem15  35609  cvmlift2lem11  35624  cvmlift2lem12  35625  cvmlift2lem13  35626  satffunlem1lem1  35713  satffunlem2lem1  35715  mvtinf  35866  eldm3  36072  elima4  36087  fvsingle  36229  snelsingles  36231  dfiota3  36232  brapply  36247  funpartlem  36253  altopeq12  36273  ranksng  36478  neibastop3  36683  tailval  36694  filnetlem4  36702  ttcid  36813  mh-inf3sn  36863  mh-infprim2bi  36868  mh-infprim3bi  36869  bj-snexg  37480  bj-restsnss  37534  bj-restsnss2  37535  f1omptsnlem  37791  f1omptsn  37792  mptsnun  37794  dissneqlem  37795  dissneq  37796  fvineqsnf1  37865  lindsadd  38073  lindsenlbs  38075  poimirlem4  38084  poimirlem25  38105  poimirlem26  38106  poimirlem27  38107  poimirlem31  38111  poimirlem32  38112  heiborlem3  38273  ismrer1  38298  lshpnel2N  39570  lsatlspsn2  39577  lsatlspsn  39578  lsatspn0  39585  lkrscss  39683  lfl1dim  39706  lfl1dim2N  39707  ldualvs  39722  atpointN  40328  watvalN  40578  trnsetN  40741  dih1dimatlem  41914  dihatexv  41923  dihjat1lem  42013  dihjat1  42014  lcfl7N  42086  lcfl8  42087  lcfl9a  42090  lcfrlem8  42134  lcfrlem9  42135  lcf1o  42136  mapdval2N  42215  mapdval4N  42217  mapdspex  42253  mapdn0  42254  mapdpglem23  42279  mapdpg  42291  mapdindp1  42305  mapdheq  42313  hvmapval  42345  mapdh9a  42374  hdmap1eq  42386  hdmap1cbv  42387  hdmapval  42413  hdmap10  42425  hdmaplkr  42498  sn-iotalem  42801  0prjspnrel  43170  mzpclval  43267  mzpcl1  43271  wopprc  43568  dnnumch3lem  43584  aomclem8  43599  mendvsca  43725  cytpval  43740  snen1g  44061  k0004lem3  44686  dvconstbi  44871  relpfrlem  45490  permaxinf2lem  45549  wessf1ornlem  45724  dvmptfprodlem  46479  fourierdlem32  46674  fourierdlem33  46675  fourierdlem48  46689  funressnmo  47601  aiotajust  47639  funressndmafv2rn  47778  fzopredsuc  47879  elsprel  48042  clnbgrval  48405  dfvopnbgr2  48436  vopnbgrel  48437  dfclnbgr6  48439  dfnbgr6  48440  cycl3grtri  48530  dmmpossx2  48920  lindslinindsimp2  49046  ldepspr  49056  ldepsnlinc  49091  line  49315  rrxline  49317  dftpos5  49456  tposideq  49470  initc  49673  setc2othin  50048  functermceu  50092  idfudiag1  50107  funcsn  50123  0fucterm  50125  mndtcval  50161  mndtcbas  50163