Theorem sneq 4578

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 2749	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2803	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4569	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4569	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1542  {cab 2715  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-sn 4569

This theorem is referenced by:  sneqi  4579  sneqd  4580  euabsn  4671  absneu  4673  preq1  4678  tpeq3  4689  issn  4776  mosneq  4786  sneqbg  4787  opeq1  4817  snexgALT  5378  propeqop  5455  opthwiener  5462  otiunsndisj  5468  opeliunxp  5691  opeliun2xp  5692  relop  5799  inisegn0  6057  xpdifid  6126  dmsnsnsn  6178  predeq123  6260  iotajust  6447  iotanul2  6465  fconstg  6721  f1osng  6816  opabiotafun  6914  fvn0ssdmfun  7020  fsng  7084  fsn2g  7085  fnressn  7105  fressnfv  7107  funfvima3  7184  f12dfv  7221  f13dfv  7222  isofrlem  7288  isoselem  7289  elxp4  7866  elxp5  7867  1stval  7937  2ndval  7938  2ndval2  7953  fo1st  7955  fo2nd  7956  f1stres  7959  f2ndres  7960  mpomptsx  8010  dmmpossx  8012  fmpox  8013  ovmptss  8036  fparlem3  8057  fparlem4  8058  xpord2pred  8088  xpord3pred  8095  suppval  8105  suppsnop  8121  ressuppssdif  8128  brtpos2  8175  dftpos4  8188  tpostpos  8189  naddcllem  8605  eceq1  8676  fvdiagfn  8832  mapsncnv  8834  elixpsn  8878  ixpsnf1o  8879  ensn1g  8962  en1  8964  difsnen  8990  xpsneng  8993  xpcomco  8998  xpassen  9002  xpdom2  9003  canth2  9061  rexdif1en  9088  cnvfi  9103  marypha2lem2  9342  cardsn  9884  pm54.43  9916  dfac5lem3  10038  dfac5lem4  10039  dfac5lem4OLD  10041  kmlem9  10072  kmlem11  10074  kmlem12  10075  ackbij1lem8  10139  r1om  10156  fictb  10157  hsmexlem4  10342  axcc2lem  10349  axcc2  10350  axdc3lem4  10366  fpwwe2cbv  10544  fpwwe2lem3  10547  fpwwecbv  10558  canth4  10561  s3iunsndisj  14921  fsum2dlem  15723  fsumcnv  15726  fsumcom2  15727  ackbijnn  15784  fprod2dlem  15936  fprodcnv  15939  fprodcom2  15940  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  lcmfunsn  16604  vdwlem1  16943  vdwlem12  16954  vdwlem13  16955  vdwnn  16960  0ram  16982  ramz2  16986  pwsval  17440  symg2bas  19359  symgfixelsi  19401  pmtrfv  19418  pmtrprfval  19453  sylow2a  19585  efgrelexlema  19715  gsum2dlem2  19937  gsum2d2  19940  gsumcom2  19941  dprdcntz  19976  dprddisj  19977  dprd2dlem2  20008  dprd2dlem1  20009  dprd2da  20010  ablfac1eu  20041  ablfaclem3  20055  lssats2  20986  lspsneq0  20998  lbsind  21067  lspsneq  21112  lspdisj2  21117  lspsnsubn0  21130  lspprat  21143  islbs2  21144  lbsextlem4  21151  lbsextg  21152  lpi0  21316  lpi1  21317  irinitoringc  21469  pzriprnglem13  21483  pzriprnglem14  21484  frlmlbs  21787  lindfind  21806  lindsind  21807  lindfrn  21811  psrvsca  21938  evlsvvval  22081  evlssca  22082  mpfind  22103  coe1fv  22180  coe1tm  22248  pf1ind  22330  submaval  22556  mdetunilem3  22589  mdetunilem4  22590  mdetunilem9  22595  islp  23115  perfi  23130  t1sncld  23301  bwth  23385  dis2ndc  23435  nllyi  23450  dissnlocfin  23504  ptbasfi  23556  txkgen  23627  xkofvcn  23659  xkoinjcn  23662  qtopeu  23691  txswaphmeolem  23779  pt1hmeo  23781  elflim2  23939  cnextfvval  24040  cnextcn  24042  cnextfres1  24043  cnextfres  24044  tsmsxplem1  24128  tsmsxplem2  24129  ucncn  24259  itg11  25668  i1faddlem  25670  i1fmullem  25671  itg1addlem3  25675  itg1mulc  25681  eldv  25875  ply1lpir  26157  areambl  26935  conway  27785  cutsval  27786  cutcuts  27787  cutbday  27790  eqcuts  27791  eqcuts2  27792  cutsun12  27796  cutbdaybnd  27801  cutbdaybnd2  27802  cutbdaylt  27804  eqcuts3  27810  bday1  27820  cuteq0  27821  cuteq1  27823  madebdaylemlrcut  27905  sltsbday  27923  cofcut1  27926  cofcutr  27930  oniso  28277  bdayn0p1  28375  expsval  28431  pw2cut2  28468  tglngval  28633  edglnl  29226  nbgrval  29419  nbgr2vtx1edg  29433  nbuhgr2vtx1edgb  29435  nbgr1vtx  29441  nb3grprlem2  29464  uvtxel  29471  uvtxel1  29479  uvtxusgrel  29486  cusgredg  29507  cplgr1v  29513  cplgr3v  29518  usgredgsscusgredg  29543  vtxdgval  29552  1loopgrvd2  29587  wlk1walk  29722  wlkres  29752  wlkp1lem8  29762  usgr2pthlem  29846  crctcshwlkn0lem6  29898  2wspiundisj  30049  clwwlknon1  30182  1wlkdlem4  30225  eupth2lem3lem3  30315  frcond1  30351  frgr1v  30356  nfrgr2v  30357  frgr3v  30360  1vwmgr  30361  3vfriswmgr  30363  3cyclfrgrrn1  30370  n4cyclfrgr  30376  frgrwopreglem4a  30395  h1de2ctlem  31641  spansn  31645  elspansn  31652  elspansn2  31653  spansneleq  31656  h1datom  31668  spansnj  31733  spansncv  31739  superpos  32440  sumdmdlem2  32505  aciunf1lem  32750  fnpreimac  32758  dfcnv2  32763  pwrssmgc  33075  gsummpt2co  33124  gsumpart  33139  gsumwrd2dccatlem  33153  gsumwrd2dccat  33154  0nellinds  33445  lindssn  33453  lsmsnidl  33474  nsgmgclem  33486  nsgmgc  33487  nsgqusf1olem1  33488  nsgqusf1olem2  33489  nsgqusf1olem3  33490  pidlnzb  33497  elrspunidl  33503  extvfval  33691  esplyfval1  33732  esplyfvaln  33733  lbslsat  33776  lindsunlem  33784  extdgval  33813  fldextrspunlsplem  33833  locfinreflem  34000  esum2dlem  34252  sibfima  34498  sibfof  34500  bnj1373  35188  bnj1489  35214  funen1cnv  35247  fineqvac  35276  cplgredgex  35319  pfxwlk  35322  revwlk  35323  loop1cycl  35335  cvmscbv  35456  cvmsdisj  35468  cvmsss2  35472  cvmliftlem15  35496  cvmlift2lem11  35511  cvmlift2lem12  35512  cvmlift2lem13  35513  satffunlem1lem1  35600  satffunlem2lem1  35602  mvtinf  35753  eldm3  35959  elima4  35974  fvsingle  36116  snelsingles  36118  dfiota3  36119  brapply  36134  funpartlem  36140  altopeq12  36160  ranksng  36365  neibastop3  36560  tailval  36571  filnetlem4  36579  ttcid  36690  mh-inf3sn  36740  mh-infprim2bi  36745  mh-infprim3bi  36746  bj-snexg  37357  bj-restsnss  37411  bj-restsnss2  37412  f1omptsnlem  37666  f1omptsn  37667  mptsnun  37669  dissneqlem  37670  dissneq  37671  fvineqsnf1  37740  lindsadd  37948  lindsenlbs  37950  poimirlem4  37959  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  poimirlem31  37986  poimirlem32  37987  heiborlem3  38148  ismrer1  38173  lshpnel2N  39445  lsatlspsn2  39452  lsatlspsn  39453  lsatspn0  39460  lkrscss  39558  lfl1dim  39581  lfl1dim2N  39582  ldualvs  39597  atpointN  40203  watvalN  40453  trnsetN  40616  dih1dimatlem  41789  dihatexv  41798  dihjat1lem  41888  dihjat1  41889  lcfl7N  41961  lcfl8  41962  lcfl9a  41965  lcfrlem8  42009  lcfrlem9  42010  lcf1o  42011  mapdval2N  42090  mapdval4N  42092  mapdspex  42128  mapdn0  42129  mapdpglem23  42154  mapdpg  42166  mapdindp1  42180  mapdheq  42188  hvmapval  42220  mapdh9a  42249  hdmap1eq  42261  hdmap1cbv  42262  hdmapval  42288  hdmap10  42300  hdmaplkr  42373  sn-iotalem  42676  evlsevl  43021  0prjspnrel  43074  mzpclval  43171  mzpcl1  43175  wopprc  43476  dnnumch3lem  43492  aomclem8  43507  mendvsca  43633  cytpval  43648  snen1g  43969  k0004lem3  44594  dvconstbi  44779  relpfrlem  45398  permaxinf2lem  45457  wessf1ornlem  45633  dvmptfprodlem  46390  fourierdlem32  46585  fourierdlem33  46586  fourierdlem48  46600  funressnmo  47506  aiotajust  47544  funressndmafv2rn  47683  fzopredsuc  47784  elsprel  47947  clnbgrval  48310  dfvopnbgr2  48341  vopnbgrel  48342  dfclnbgr6  48344  dfnbgr6  48345  cycl3grtri  48435  dmmpossx2  48825  lindslinindsimp2  48951  ldepspr  48961  ldepsnlinc  48996  line  49220  rrxline  49222  dftpos5  49361  tposideq  49375  initc  49578  setc2othin  49953  functermceu  49997  idfudiag1  50012  funcsn  50028  0fucterm  50030  mndtcval  50066  mndtcbas  50068