Theorem sneq 4594

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-sn 4585

This theorem is used by:  sneqi  4595  sneqd  4596  euabsn  4687  absneu  4689  preq1  4694  tpeq3  4705  issn  4792  mosneq  4802  sneqbg  4803  opeq1  4833  snexgALT  5399  propeqop  5479  opthwiener  5487  otiunsndisj  5493  opeliunxp  5718  opeliun2xp  5719  relop  5828  inisegn0  6096  xpdifid  6159  xpdifcnvepel  6160  dmsnsnsn  6220  predeq123  6304  iotajust  6492  iotanul2  6510  fconstg  6767  f1osng  6865  opabiotafun  6963  fvn0ssdmfun  7072  fsng  7136  fsn2g  7137  fnressn  7160  fressnfv  7162  funfvima3  7240  f12dfv  7279  f13dfv  7280  isofrlem  7346  isoselem  7347  elxp4  7932  elxp5  7933  1stval  8001  2ndval  8002  2ndval2  8017  fo1st  8019  fo2nd  8020  f1stres  8023  f2ndres  8024  mpomptsx  8073  dmmpossx  8075  fmpox  8076  ovmptss  8102  fparlem3  8123  fparlem4  8124  xpord2pred  8155  xpord3pred  8162  suppval  8172  suppsnop  8188  ressuppssdif  8195  brtpos2  8242  dftpos4  8255  tpostpos  8256  naddcllem  8678  eceq1  8750  fvdiagfn  8912  mapsncnv  8914  elixpsn  8958  ixpsnf1o  8959  ensn1g  9042  en1  9044  funen1cnv  9049  difsnen  9071  xpsneng  9074  xpcomco  9079  xpassen  9083  xpdom2  9084  canth2  9142  rexdif1en  9169  cnvfi  9184  marypha2lem2  9421  ranksng  9867  cardsn  10043  pm54.43  10075  dfac5lem3  10197  dfac5lem4  10198  kmlem9  10230  kmlem11  10232  kmlem12  10233  ackbij1lem8  10297  hfom  10314  fictb  10315  hsmexlem4  10500  axcc2lem  10507  axcc2  10508  axdc3lem4  10524  fpwwe2cbv  10708  fpwwe2lem3  10711  fpwwecbv  10722  canth4  10725  s3iunsndisj  15114  fsum2dlem  15929  fsumcnv  15932  fsumcom2  15933  ackbijnn  15990  fprod2dlem  16140  fprodcnv  16143  fprodcom2  16144  lcmfunsnlem1  16805  lcmfunsnlem2lem1  16806  lcmfunsnlem2lem2  16807  lcmfunsnlem2  16808  lcmfunsn  16812  vdwlem1  17152  vdwlem12  17163  vdwlem13  17164  vdwnn  17169  0ram  17191  ramz2  17195  pwsval  17650  symg2bas  19600  symgfixelsi  19642  pmtrfv  19659  pmtrprfval  19694  sylow2a  19826  efgrelexlema  19956  gsum2dlem2  20178  gsum2d2  20181  gsumcom2  20182  dprdcntz  20217  dprddisj  20218  dprd2dlem2  20249  dprd2dlem1  20250  dprd2da  20251  ablfac1eu  20282  ablfaclem3  20296  lssats2  21268  lspsneq0  21280  lbsind  21348  lspsneq  21393  lspdisj2  21398  lspsnsubn0  21411  lspprat  21424  islbs2  21425  lbsextlem4  21432  lbsextg  21433  lpi0  21643  lpi1  21644  irinitoringc  21778  pzriprnglem13  21792  pzriprnglem14  21793  frlmlbs  22096  lindfind  22115  lindsind  22116  lindfrn  22120  lindsenlbs  22150  psrvsca  22250  evlsvvval  22395  evlssca  22396  mpfind  22417  evlsevl  22434  coe1fv  22517  coe1tm  22585  pf1ind  22666  submaval  22889  mdetunilem3  22922  mdetunilem4  22923  mdetunilem9  22928  islp  23451  perfi  23466  t1sncld  23637  bwth  23721  dis2ndc  23772  nllyi  23787  dissnlocfin  23841  ptbasfi  23893  txkgen  23964  xkofvcn  23996  xkoinjcn  23999  qtopeu  24028  txswaphmeolem  24116  pt1hmeo  24118  elflim2  24276  cnextfvval  24377  cnextcn  24379  cnextfres1  24380  cnextfres  24381  tsmsxplem1  24465  tsmsxplem2  24466  ucncn  24596  itg11  26005  i1faddlem  26007  i1fmullem  26008  itg1addlem3  26012  itg1mulc  26018  eldv  26211  ply1lpir  26493  areambl  27279  conway  28158  cutsval  28159  cutcuts  28160  cutbday  28163  eqcuts  28164  eqcuts2  28165  cutsun12  28169  cutbdaybnd  28174  cutbdaybnd2  28175  cutbdaylt  28177  eqcuts3  28183  bday1  28193  cuteq0  28194  cuteq1  28196  madebdaylemlrcut  28278  sltsbday  28296  cofcut1  28299  cofcutr  28303  oniso  28650  bdayn0p1  28748  expsval  28804  pw2cut2  28841  tglngval  29007  edglnl  29714  nbgrval  29910  nbgr2vtx1edg  29924  nbuhgr2vtx1edgb  29926  nbgr1vtx  29932  nb3grprlem2  29955  uvtxel  29962  uvtxel1  29970  uvtxusgrel  29977  cusgredg  29998  cplgr1v  30004  cplgr3v  30009  usgredgsscusgredg  30033  vtxdgval  30042  1loopgrvd2  30077  wlk1walk  30212  wlkres  30242  wlkp1lem8  30252  pfxwlk  30259  revwlk  30260  usgr2pthlem  30342  crctcshwlkn0lem6  30397  2wspiundisj  30548  clwwlknon1  30681  1wlkdlem4  30724  loop1cycl  30737  eupth2lem3lem3  30824  frcond1  30860  frgr1v  30865  nfrgr2v  30866  frgr3v  30869  1vwmgr  30870  3vfriswmgr  30872  3cyclfrgrrn1  30879  n4cyclfrgr  30885  frgrwopreglem4a  30904  h1de2ctlem  32150  spansn  32154  elspansn  32161  elspansn2  32162  spansneleq  32165  h1datom  32177  spansnj  32242  spansncv  32248  superpos  32949  sumdmdlem2  33014  aciunf1lem  33249  fnpreimac  33257  dfcnv2  33262  pwrssmgc  33554  gsummpt2co  33602  gsumpart  33617  gsumwrd2dccatlem  33631  gsumwrd2dccat  33632  0nellinds  33919  lindssn  33926  lsmsnidl  33945  nsgmgclem  33955  nsgmgc  33956  nsgqusf1olem1  33957  nsgqusf1olem2  33958  nsgqusf1olem3  33959  pidlnzb  33965  elrspunidl  33971  extvfval  34157  esplyfval1  34198  esplyfvaln  34199  lbslsat  34241  lindsunlem  34249  extdgval  34278  fldextrspunlsplem  34298  locfinreflem  34465  esum2dlem  34717  sibfima  34963  sibfof  34965  bnj1373  35653  bnj1489  35679  fineqvac  35767  onvfowev  35878  cplgredgex  35884  cvmscbv  36002  cvmsdisj  36014  cvmsss2  36018  cvmliftlem15  36042  cvmlift2lem11  36057  cvmlift2lem12  36058  cvmlift2lem13  36059  satffunlem1lem1  36146  satffunlem2lem1  36148  mvtinf  36299  eldm3  36505  elima4  36520  fvsingle  36662  snelsingles  36664  dfiota3  36665  brapply  36680  funpartlem  36686  altopeq12  36707  neibastop3  37130  tailval  37141  filnetlem4  37149  ttcid  37260  mh-inf3sn  37310  mh-infprim2bi  37315  mh-infprim3bi  37316  bj-snexg  37927  bj-restsnss  37984  bj-restsnss2  37985  f1omptsnlem  38239  f1omptsn  38240  mptsnun  38242  dissneqlem  38243  dissneq  38244  fvineqsnf1  38313  lindsadd  38516  poimirlem4  38522  poimirlem25  38543  poimirlem26  38544  poimirlem27  38545  poimirlem31  38549  poimirlem32  38550  heiborlem3  38727  ismrer1  38752  lshpnel2N  40022  lsatlspsn2  40029  lsatlspsn  40030  lsatspn0  40037  lkrscss  40135  lfl1dim  40158  lfl1dim2N  40159  ldualvs  40174  atpointN  40780  watvalN  41030  trnsetN  41193  dih1dimatlem  42366  dihatexv  42375  dihjat1lem  42465  dihjat1  42466  lcfl7N  42538  lcfl8  42539  lcfl9a  42542  lcfrlem8  42586  lcfrlem9  42587  lcf1o  42588  mapdval2N  42667  mapdval4N  42669  mapdspex  42705  mapdn0  42706  mapdpglem23  42731  mapdpg  42743  mapdindp1  42757  mapdheq  42765  hvmapval  42797  mapdh9a  42826  hdmap1eq  42838  hdmap1cbv  42839  hdmapval  42865  hdmap10  42877  hdmaplkr  42950  sn-iotalem  43255  0prjspnrel  43643  mzpclval  43715  mzpcl1  43719  wopprc  44016  dnnumch3lem  44032  aomclem8  44047  mendvsca  44173  cytpval  44188  snen1g  44509  k0004lem3  45134  dvconstbi  45303  relpfrlem  45921  permaxinf2lem  45980  wessf1ornlem  46169  dvmptfprodlem  46923  fourierdlem32  47118  fourierdlem33  47119  fourierdlem48  47133  funressnmo  48085  aiotajust  48123  funressndmafv2rn  48262  fzopredsuc  48363  elsprel  48526  clnbgrval  48889  dfvopnbgr2  48920  vopnbgrel  48921  dfclnbgr6  48923  dfnbgr6  48924  cycl3grtri  49014  dmmpossx2  49418  lindslinindsimp2  49544  ldepspr  49554  ldepsnlinc  49589  line  49813  rrxline  49815  dftpos5  49951  tposideq  49965  initc  50168  setc2othin  50543  functermceu  50587  idfudiag1  50602  funcsn  50618  0fucterm  50620  mndtcval  50656  mndtcbaseu  50658