Theorem sneq 4565

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 2751	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2805	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4556	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4556	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2799	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1547  {cab 2717  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-sn 4556

This theorem is referenced by:  sneqi  4566  sneqd  4567  euabsn  4658  absneu  4660  preq1  4665  tpeq3  4676  issn  4763  mosneq  4773  sneqbg  4774  opeq1  4804  snexgALT  5370  propeqop  5448  opthwiener  5455  otiunsndisj  5461  opeliunxp  5685  opeliun2xp  5686  relop  5792  inisegn0  6050  xpdifid  6119  dmsnsnsn  6171  predeq123  6253  iotajust  6440  iotanul2  6458  fconstg  6714  f1osng  6809  opabiotafun  6907  fvn0ssdmfun  7015  fsng  7079  fsn2g  7080  fnressn  7101  fressnfv  7103  funfvima3  7180  f12dfv  7217  f13dfv  7218  isofrlem  7284  isoselem  7285  elxp4  7862  elxp5  7863  1stval  7933  2ndval  7934  2ndval2  7949  fo1st  7951  fo2nd  7952  f1stres  7955  f2ndres  7956  mpomptsx  8006  dmmpossx  8008  fmpox  8009  ovmptss  8032  fparlem3  8053  fparlem4  8054  xpord2pred  8085  xpord3pred  8092  suppval  8102  suppsnop  8118  ressuppssdif  8125  brtpos2  8172  dftpos4  8185  tpostpos  8186  naddcllem  8602  eceq1  8673  fvdiagfn  8829  mapsncnv  8831  elixpsn  8875  ixpsnf1o  8876  ensn1g  8959  en1  8961  difsnen  8987  xpsneng  8990  xpcomco  8995  xpassen  8999  xpdom2  9000  canth2  9058  rexdif1en  9085  cnvfi  9100  marypha2lem2  9339  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  20990  lspsneq0  21002  lbsind  21070  lspsneq  21115  lspdisj2  21120  lspsnsubn0  21133  lspprat  21146  islbs2  21147  lbsextlem4  21154  lbsextg  21155  lpi0  21319  lpi1  21320  irinitoringc  21454  pzriprnglem13  21468  pzriprnglem14  21469  frlmlbs  21772  lindfind  21791  lindsind  21792  lindfrn  21796  psrvsca  21924  evlsvvval  22069  evlssca  22070  mpfind  22091  evlsevl  22108  coe1fv  22191  coe1tm  22259  pf1ind  22341  submaval  22564  mdetunilem3  22597  mdetunilem4  22598  mdetunilem9  22603  islp  23123  perfi  23138  t1sncld  23309  bwth  23393  dis2ndc  23443  nllyi  23458  dissnlocfin  23512  ptbasfi  23564  txkgen  23635  xkofvcn  23667  xkoinjcn  23670  qtopeu  23699  txswaphmeolem  23787  pt1hmeo  23789  elflim2  23947  cnextfvval  24048  cnextcn  24050  cnextfres1  24051  cnextfres  24052  tsmsxplem1  24136  tsmsxplem2  24137  ucncn  24267  itg11  25676  i1faddlem  25678  i1fmullem  25679  itg1addlem3  25683  itg1mulc  25689  eldv  25883  ply1lpir  26165  areambl  26940  conway  27789  cutsval  27790  cutcuts  27791  cutbday  27794  eqcuts  27795  eqcuts2  27796  cutsun12  27800  cutbdaybnd  27805  cutbdaybnd2  27806  cutbdaylt  27808  eqcuts3  27814  bday1  27824  cuteq0  27825  cuteq1  27827  madebdaylemlrcut  27909  sltsbday  27927  cofcut1  27930  cofcutr  27934  oniso  28281  bdayn0p1  28379  expsval  28435  pw2cut2  28472  tglngval  28637  edglnl  29230  nbgrval  29423  nbgr2vtx1edg  29437  nbuhgr2vtx1edgb  29439  nbgr1vtx  29445  nb3grprlem2  29468  uvtxel  29475  uvtxel1  29483  uvtxusgrel  29490  cusgredg  29511  cplgr1v  29517  cplgr3v  29522  usgredgsscusgredg  29546  vtxdgval  29555  1loopgrvd2  29590  wlk1walk  29725  wlkres  29755  wlkp1lem8  29765  usgr2pthlem  29849  crctcshwlkn0lem6  29901  2wspiundisj  30052  clwwlknon1  30185  1wlkdlem4  30228  eupth2lem3lem3  30318  frcond1  30354  frgr1v  30359  nfrgr2v  30360  frgr3v  30363  1vwmgr  30364  3vfriswmgr  30366  3cyclfrgrrn1  30373  n4cyclfrgr  30379  frgrwopreglem4a  30398  h1de2ctlem  31644  spansn  31648  elspansn  31655  elspansn2  31656  spansneleq  31659  h1datom  31671  spansnj  31736  spansncv  31742  superpos  32443  sumdmdlem2  32508  aciunf1lem  32754  fnpreimac  32762  dfcnv2  32767  pwrssmgc  33079  gsummpt2co  33129  gsumpart  33144  gsumwrd2dccatlem  33158  gsumwrd2dccat  33159  0nellinds  33453  lindssn  33461  lsmsnidl  33482  nsgmgclem  33494  nsgmgc  33495  nsgqusf1olem1  33496  nsgqusf1olem2  33497  nsgqusf1olem3  33498  pidlnzb  33505  elrspunidl  33511  extvfval  33716  esplyfval1  33757  esplyfvaln  33758  lbslsat  33800  lindsunlem  33808  extdgval  33837  fldextrspunlsplem  33857  locfinreflem  34024  esum2dlem  34276  sibfima  34522  sibfof  34524  bnj1373  35212  bnj1489  35238  funen1cnv  35269  fineqvac  35297  cplgredgex  35349  pfxwlk  35352  revwlk  35353  loop1cycl  35365  cvmscbv  35486  cvmsdisj  35498  cvmsss2  35502  cvmliftlem15  35526  cvmlift2lem11  35541  cvmlift2lem12  35542  cvmlift2lem13  35543  satffunlem1lem1  35630  satffunlem2lem1  35632  mvtinf  35783  eldm3  35989  elima4  36004  fvsingle  36146  snelsingles  36148  dfiota3  36149  brapply  36164  funpartlem  36170  altopeq12  36190  ranksng  36395  neibastop3  36590  tailval  36601  filnetlem4  36609  ttcid  36720  mh-inf3sn  36770  mh-infprim2bi  36775  mh-infprim3bi  36776  bj-snexg  37387  bj-restsnss  37441  bj-restsnss2  37442  f1omptsnlem  37698  f1omptsn  37699  mptsnun  37701  dissneqlem  37702  dissneq  37703  fvineqsnf1  37772  lindsadd  37980  lindsenlbs  37982  poimirlem4  37991  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimirlem31  38018  poimirlem32  38019  heiborlem3  38180  ismrer1  38205  lshpnel2N  39477  lsatlspsn2  39484  lsatlspsn  39485  lsatspn0  39492  lkrscss  39590  lfl1dim  39613  lfl1dim2N  39614  ldualvs  39629  atpointN  40235  watvalN  40485  trnsetN  40648  dih1dimatlem  41821  dihatexv  41830  dihjat1lem  41920  dihjat1  41921  lcfl7N  41993  lcfl8  41994  lcfl9a  41997  lcfrlem8  42041  lcfrlem9  42042  lcf1o  42043  mapdval2N  42122  mapdval4N  42124  mapdspex  42160  mapdn0  42161  mapdpglem23  42186  mapdpg  42198  mapdindp1  42212  mapdheq  42220  hvmapval  42252  mapdh9a  42281  hdmap1eq  42293  hdmap1cbv  42294  hdmapval  42320  hdmap10  42332  hdmaplkr  42405  sn-iotalem  42708  0prjspnrel  43077  mzpclval  43174  mzpcl1  43178  wopprc  43475  dnnumch3lem  43491  aomclem8  43506  mendvsca  43632  cytpval  43647  snen1g  43968  k0004lem3  44593  dvconstbi  44778  relpfrlem  45397  permaxinf2lem  45456  wessf1ornlem  45632  dvmptfprodlem  46387  fourierdlem32  46582  fourierdlem33  46583  fourierdlem48  46597  funressnmo  47509  aiotajust  47547  funressndmafv2rn  47686  fzopredsuc  47787  elsprel  47950  clnbgrval  48313  dfvopnbgr2  48344  vopnbgrel  48345  dfclnbgr6  48347  dfnbgr6  48348  cycl3grtri  48438  dmmpossx2  48828  lindslinindsimp2  48954  ldepspr  48964  ldepsnlinc  48999  line  49223  rrxline  49225  dftpos5  49364  tposideq  49378  initc  49581  setc2othin  49956  functermceu  50000  idfudiag1  50015  funcsn  50031  0fucterm  50033  mndtcval  50069  mndtcbas  50071