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

Syntax hints:   → wi 4   = wceq 1540  {cab 2707  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-sn 4580

This theorem is referenced by:  sneqi  4590  sneqd  4591  euabsn  4680  absneu  4682  preq1  4687  tpeq3  4698  issn  4786  mosneq  4796  sneqbg  4797  opeq1  4827  snexg  5377  propeqop  5454  opthwiener  5461  otiunsndisj  5467  opeliunxp  5690  opeliun2xp  5691  relop  5797  inisegn0  6053  xpdifid  6121  dmsnsnsn  6173  predeq123  6254  iotajust  6441  iotanul2  6459  fconstg  6715  f1osng  6809  opabiotafun  6907  fvn0ssdmfun  7012  fsng  7075  fsn2g  7076  fnressn  7096  fressnfv  7098  funfvima3  7176  f12dfv  7214  f13dfv  7215  isofrlem  7281  isoselem  7282  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  8033  fparlem3  8054  fparlem4  8055  xpord2pred  8085  xpord3pred  8092  suppval  8102  suppsnop  8118  ressuppssdif  8125  brtpos2  8172  dftpos4  8185  tpostpos  8186  naddcllem  8601  eceq1  8671  fvdiagfn  8825  mapsncnv  8827  elixpsn  8871  ixpsnf1o  8872  ensn1g  8954  en1  8956  difsnen  8983  xpsneng  8986  xpcomco  8991  xpassen  8995  xpdom2  8996  canth2  9054  rexdif1en  9082  rexdif1enOLD  9083  cnvfi  9100  xpfiOLD  9228  marypha2lem2  9345  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  10543  fpwwe2lem3  10546  fpwwecbv  10557  canth4  10560  s3iunsndisj  14893  fsum2dlem  15695  fsumcnv  15698  fsumcom2  15699  ackbijnn  15753  fprod2dlem  15905  fprodcnv  15908  fprodcom2  15909  lcmfunsnlem1  16566  lcmfunsnlem2lem1  16567  lcmfunsnlem2lem2  16568  lcmfunsnlem2  16569  lcmfunsn  16573  vdwlem1  16911  vdwlem12  16922  vdwlem13  16923  vdwnn  16928  0ram  16950  ramz2  16954  pwsval  17408  symg2bas  19290  symgfixelsi  19332  pmtrfv  19349  pmtrprfval  19384  sylow2a  19516  efgrelexlema  19646  gsum2dlem2  19868  gsum2d2  19871  gsumcom2  19872  dprdcntz  19907  dprddisj  19908  dprd2dlem2  19939  dprd2dlem1  19940  dprd2da  19941  ablfac1eu  19972  ablfaclem3  19986  lssats2  20921  lspsneq0  20933  lbsind  21002  lspsneq  21047  lspdisj2  21052  lspsnsubn0  21065  lspprat  21078  islbs2  21079  lbsextlem4  21086  lbsextg  21087  lpi0  21251  lpi1  21252  irinitoringc  21404  pzriprnglem13  21418  pzriprnglem14  21419  frlmlbs  21722  lindfind  21741  lindsind  21742  lindfrn  21746  psrvsca  21874  evlssca  22012  mpfind  22030  coe1fv  22107  coe1tm  22175  pf1ind  22258  submaval  22484  mdetunilem3  22517  mdetunilem4  22518  mdetunilem9  22523  islp  23043  perfi  23058  t1sncld  23229  bwth  23313  dis2ndc  23363  nllyi  23378  dissnlocfin  23432  ptbasfi  23484  txkgen  23555  xkofvcn  23587  xkoinjcn  23590  qtopeu  23619  txswaphmeolem  23707  pt1hmeo  23709  elflim2  23867  cnextfvval  23968  cnextcn  23970  cnextfres1  23971  cnextfres  23972  tsmsxplem1  24056  tsmsxplem2  24057  ucncn  24188  itg11  25608  i1faddlem  25610  i1fmullem  25611  itg1addlem3  25615  itg1mulc  25621  eldv  25815  ply1lpir  26103  areambl  26884  conway  27728  scutval  27729  scutcut  27730  scutbday  27733  eqscut  27734  eqscut2  27735  scutun12  27739  scutbdaybnd  27744  scutbdaybnd2  27745  scutbdaylt  27747  eqscut3  27753  bday1s  27763  cuteq0  27764  cuteq1  27766  madebdaylemlrcut  27831  cofcut1  27851  cofcutr  27855  onsiso  28192  bdayn0p1  28281  expsval  28335  tglngval  28514  edglnl  29106  nbgrval  29299  nbgr2vtx1edg  29313  nbuhgr2vtx1edgb  29315  nbgr1vtx  29321  nb3grprlem2  29344  uvtxel  29351  uvtxel1  29359  uvtxusgrel  29366  cusgredg  29387  cplgr1v  29393  cplgr3v  29398  usgredgsscusgredg  29423  vtxdgval  29432  1loopgrvd2  29467  wlk1walk  29602  wlkres  29632  wlkp1lem8  29642  usgr2pthlem  29726  crctcshwlkn0lem6  29778  2wspiundisj  29926  clwwlknon1  30059  1wlkdlem4  30102  eupth2lem3lem3  30192  frcond1  30228  frgr1v  30233  nfrgr2v  30234  frgr3v  30237  1vwmgr  30238  3vfriswmgr  30240  3cyclfrgrrn1  30247  n4cyclfrgr  30253  frgrwopreglem4a  30272  h1de2ctlem  31517  spansn  31521  elspansn  31528  elspansn2  31529  spansneleq  31532  h1datom  31544  spansnj  31609  spansncv  31615  superpos  32316  sumdmdlem2  32381  aciunf1lem  32619  fnpreimac  32628  dfcnv2  32633  pwrssmgc  32955  gsummpt2co  33014  gsumpart  33023  gsumwrd2dccatlem  33032  gsumwrd2dccat  33033  0nellinds  33320  lindssn  33328  lsmsnidl  33349  nsgmgclem  33361  nsgmgc  33362  nsgqusf1olem1  33363  nsgqusf1olem2  33364  nsgqusf1olem3  33365  pidlnzb  33372  elrspunidl  33378  lbslsat  33591  lindsunlem  33599  extdgval  33628  fldextrspunlsplem  33647  locfinreflem  33809  esum2dlem  34061  sibfima  34308  sibfof  34310  bnj1373  34999  bnj1489  35025  funen1cnv  35057  fineqvac  35074  cplgredgex  35096  pfxwlk  35099  revwlk  35100  loop1cycl  35112  cvmscbv  35233  cvmsdisj  35245  cvmsss2  35249  cvmliftlem15  35273  cvmlift2lem11  35288  cvmlift2lem12  35289  cvmlift2lem13  35290  satffunlem1lem1  35377  satffunlem2lem1  35379  mvtinf  35530  eldm3  35736  elima4  35751  fvsingle  35896  snelsingles  35898  dfiota3  35899  brapply  35914  funpartlem  35918  altopeq12  35938  ranksng  36143  neibastop3  36338  tailval  36349  filnetlem4  36357  bj-snexg  37010  bj-restsnss  37059  bj-restsnss2  37060  f1omptsnlem  37312  f1omptsn  37313  mptsnun  37315  dissneqlem  37316  dissneq  37317  fvineqsnf1  37386  lindsadd  37595  lindsenlbs  37597  poimirlem4  37606  poimirlem25  37627  poimirlem26  37628  poimirlem27  37629  poimirlem31  37633  poimirlem32  37634  heiborlem3  37795  ismrer1  37820  lshpnel2N  38966  lsatlspsn2  38973  lsatlspsn  38974  lsatspn0  38981  lkrscss  39079  lfl1dim  39102  lfl1dim2N  39103  ldualvs  39118  atpointN  39725  watvalN  39975  trnsetN  40138  dih1dimatlem  41311  dihatexv  41320  dihjat1lem  41410  dihjat1  41411  lcfl7N  41483  lcfl8  41484  lcfl9a  41487  lcfrlem8  41531  lcfrlem9  41532  lcf1o  41533  mapdval2N  41612  mapdval4N  41614  mapdspex  41650  mapdn0  41651  mapdpglem23  41676  mapdpg  41688  mapdindp1  41702  mapdheq  41710  hvmapval  41742  mapdh9a  41771  hdmap1eq  41783  hdmap1cbv  41784  hdmapval  41810  hdmap10  41822  hdmaplkr  41895  sn-iotalem  42197  evlsvvval  42539  evlsevl  42547  0prjspnrel  42603  mzpclval  42701  mzpcl1  42705  wopprc  43006  dnnumch3lem  43022  aomclem8  43037  mendvsca  43163  cytpval  43178  snen1g  43500  k0004lem3  44125  dvconstbi  44310  relpfrlem  44930  permaxinf2lem  44989  wessf1ornlem  45166  dvmptfprodlem  45929  fourierdlem32  46124  fourierdlem33  46125  fourierdlem48  46139  funressnmo  47034  aiotajust  47072  funressndmafv2rn  47211  fzopredsuc  47311  elsprel  47463  clnbgrval  47810  dfvopnbgr2  47841  vopnbgrel  47842  dfclnbgr6  47844  dfnbgr6  47845  cycl3grtri  47935  dmmpossx2  48325  lindslinindsimp2  48452  ldepspr  48462  ldepsnlinc  48497  line  48721  rrxline  48723  dftpos5  48862  tposideq  48876  initc  49080  setc2othin  49455  functermceu  49499  idfudiag1  49514  funcsn  49530  0fucterm  49532  mndtcval  49568  mndtcbas  49570