Theorem sneq 4587

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

Syntax hints:   → wi 4   = wceq 1541  {cab 2711  {csn 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-sn 4578

This theorem is referenced by:  sneqi  4588  sneqd  4589  euabsn  4680  absneu  4682  preq1  4687  tpeq3  4698  issn  4785  mosneq  4795  sneqbg  4796  opeq1  4826  snexg  5377  propeqop  5452  opthwiener  5459  otiunsndisj  5465  opeliunxp  5688  opeliun2xp  5689  relop  5796  inisegn0  6054  xpdifid  6123  dmsnsnsn  6175  predeq123  6257  iotajust  6444  iotanul2  6462  fconstg  6718  f1osng  6813  opabiotafun  6911  fvn0ssdmfun  7016  fsng  7079  fsn2g  7080  fnressn  7100  fressnfv  7102  funfvima3  7179  f12dfv  7216  f13dfv  7217  isofrlem  7283  isoselem  7284  elxp4  7861  elxp5  7862  1stval  7932  2ndval  7933  2ndval2  7948  fo1st  7950  fo2nd  7951  f1stres  7954  f2ndres  7955  mpomptsx  8005  dmmpossx  8007  fmpox  8008  ovmptss  8032  fparlem3  8053  fparlem4  8054  xpord2pred  8084  xpord3pred  8091  suppval  8101  suppsnop  8117  ressuppssdif  8124  brtpos2  8171  dftpos4  8184  tpostpos  8185  naddcllem  8600  eceq1  8670  fvdiagfn  8825  mapsncnv  8827  elixpsn  8871  ixpsnf1o  8872  ensn1g  8955  en1  8957  difsnen  8983  xpsneng  8986  xpcomco  8991  xpassen  8995  xpdom2  8996  canth2  9054  rexdif1en  9081  cnvfi  9096  marypha2lem2  9331  cardsn  9873  pm54.43  9905  dfac5lem3  10027  dfac5lem4  10028  dfac5lem4OLD  10030  kmlem9  10061  kmlem11  10063  kmlem12  10064  ackbij1lem8  10128  r1om  10145  fictb  10146  hsmexlem4  10331  axcc2lem  10338  axcc2  10339  axdc3lem4  10355  fpwwe2cbv  10532  fpwwe2lem3  10535  fpwwecbv  10546  canth4  10549  s3iunsndisj  14882  fsum2dlem  15684  fsumcnv  15687  fsumcom2  15688  ackbijnn  15742  fprod2dlem  15894  fprodcnv  15897  fprodcom2  15898  lcmfunsnlem1  16555  lcmfunsnlem2lem1  16556  lcmfunsnlem2lem2  16557  lcmfunsnlem2  16558  lcmfunsn  16562  vdwlem1  16900  vdwlem12  16911  vdwlem13  16912  vdwnn  16917  0ram  16939  ramz2  16943  pwsval  17397  symg2bas  19313  symgfixelsi  19355  pmtrfv  19372  pmtrprfval  19407  sylow2a  19539  efgrelexlema  19669  gsum2dlem2  19891  gsum2d2  19894  gsumcom2  19895  dprdcntz  19930  dprddisj  19931  dprd2dlem2  19962  dprd2dlem1  19963  dprd2da  19964  ablfac1eu  19995  ablfaclem3  20009  lssats2  20942  lspsneq0  20954  lbsind  21023  lspsneq  21068  lspdisj2  21073  lspsnsubn0  21086  lspprat  21099  islbs2  21100  lbsextlem4  21107  lbsextg  21108  lpi0  21272  lpi1  21273  irinitoringc  21425  pzriprnglem13  21439  pzriprnglem14  21440  frlmlbs  21743  lindfind  21762  lindsind  21763  lindfrn  21767  psrvsca  21896  evlsvvval  22039  evlssca  22040  mpfind  22061  coe1fv  22138  coe1tm  22206  pf1ind  22290  submaval  22516  mdetunilem3  22549  mdetunilem4  22550  mdetunilem9  22555  islp  23075  perfi  23090  t1sncld  23261  bwth  23345  dis2ndc  23395  nllyi  23410  dissnlocfin  23464  ptbasfi  23516  txkgen  23587  xkofvcn  23619  xkoinjcn  23622  qtopeu  23651  txswaphmeolem  23739  pt1hmeo  23741  elflim2  23899  cnextfvval  24000  cnextcn  24002  cnextfres1  24003  cnextfres  24004  tsmsxplem1  24088  tsmsxplem2  24089  ucncn  24219  itg11  25639  i1faddlem  25641  i1fmullem  25642  itg1addlem3  25646  itg1mulc  25652  eldv  25846  ply1lpir  26134  areambl  26915  conway  27760  scutval  27761  scutcut  27762  scutbday  27765  eqscut  27766  eqscut2  27767  scutun12  27771  scutbdaybnd  27776  scutbdaybnd2  27777  scutbdaylt  27779  eqscut3  27785  bday1s  27795  cuteq0  27796  cuteq1  27798  madebdaylemlrcut  27864  cofcut1  27884  cofcutr  27888  onsiso  28225  bdayn0p1  28314  expsval  28368  pw2cut2  28402  tglngval  28549  edglnl  29142  nbgrval  29335  nbgr2vtx1edg  29349  nbuhgr2vtx1edgb  29351  nbgr1vtx  29357  nb3grprlem2  29380  uvtxel  29387  uvtxel1  29395  uvtxusgrel  29402  cusgredg  29423  cplgr1v  29429  cplgr3v  29434  usgredgsscusgredg  29459  vtxdgval  29468  1loopgrvd2  29503  wlk1walk  29638  wlkres  29668  wlkp1lem8  29678  usgr2pthlem  29762  crctcshwlkn0lem6  29814  2wspiundisj  29965  clwwlknon1  30098  1wlkdlem4  30141  eupth2lem3lem3  30231  frcond1  30267  frgr1v  30272  nfrgr2v  30273  frgr3v  30276  1vwmgr  30277  3vfriswmgr  30279  3cyclfrgrrn1  30286  n4cyclfrgr  30292  frgrwopreglem4a  30311  h1de2ctlem  31556  spansn  31560  elspansn  31567  elspansn2  31568  spansneleq  31571  h1datom  31583  spansnj  31648  spansncv  31654  superpos  32355  sumdmdlem2  32420  aciunf1lem  32666  fnpreimac  32675  dfcnv2  32680  pwrssmgc  33010  gsummpt2co  33059  gsumpart  33074  gsumwrd2dccatlem  33087  gsumwrd2dccat  33088  0nellinds  33379  lindssn  33387  lsmsnidl  33408  nsgmgclem  33420  nsgmgc  33421  nsgqusf1olem1  33422  nsgqusf1olem2  33423  nsgqusf1olem3  33424  pidlnzb  33431  elrspunidl  33437  extvfval  33625  lbslsat  33701  lindsunlem  33709  extdgval  33738  fldextrspunlsplem  33758  locfinreflem  33925  esum2dlem  34177  sibfima  34423  sibfof  34425  bnj1373  35114  bnj1489  35140  funen1cnv  35172  fineqvac  35211  cplgredgex  35237  pfxwlk  35240  revwlk  35241  loop1cycl  35253  cvmscbv  35374  cvmsdisj  35386  cvmsss2  35390  cvmliftlem15  35414  cvmlift2lem11  35429  cvmlift2lem12  35430  cvmlift2lem13  35431  satffunlem1lem1  35518  satffunlem2lem1  35520  mvtinf  35671  eldm3  35877  elima4  35892  fvsingle  36034  snelsingles  36036  dfiota3  36037  brapply  36052  funpartlem  36058  altopeq12  36078  ranksng  36283  neibastop3  36478  tailval  36489  filnetlem4  36497  bj-snexg  37151  bj-restsnss  37200  bj-restsnss2  37201  f1omptsnlem  37453  f1omptsn  37454  mptsnun  37456  dissneqlem  37457  dissneq  37458  fvineqsnf1  37527  lindsadd  37726  lindsenlbs  37728  poimirlem4  37737  poimirlem25  37758  poimirlem26  37759  poimirlem27  37760  poimirlem31  37764  poimirlem32  37765  heiborlem3  37926  ismrer1  37951  lshpnel2N  39157  lsatlspsn2  39164  lsatlspsn  39165  lsatspn0  39172  lkrscss  39270  lfl1dim  39293  lfl1dim2N  39294  ldualvs  39309  atpointN  39915  watvalN  40165  trnsetN  40328  dih1dimatlem  41501  dihatexv  41510  dihjat1lem  41600  dihjat1  41601  lcfl7N  41673  lcfl8  41674  lcfl9a  41677  lcfrlem8  41721  lcfrlem9  41722  lcf1o  41723  mapdval2N  41802  mapdval4N  41804  mapdspex  41840  mapdn0  41841  mapdpglem23  41866  mapdpg  41878  mapdindp1  41892  mapdheq  41900  hvmapval  41932  mapdh9a  41961  hdmap1eq  41973  hdmap1cbv  41974  hdmapval  42000  hdmap10  42012  hdmaplkr  42085  sn-iotalem  42392  evlsevl  42732  0prjspnrel  42785  mzpclval  42882  mzpcl1  42886  wopprc  43187  dnnumch3lem  43203  aomclem8  43218  mendvsca  43344  cytpval  43359  snen1g  43681  k0004lem3  44306  dvconstbi  44491  relpfrlem  45110  permaxinf2lem  45169  wessf1ornlem  45345  dvmptfprodlem  46104  fourierdlem32  46299  fourierdlem33  46300  fourierdlem48  46314  funressnmo  47208  aiotajust  47246  funressndmafv2rn  47385  fzopredsuc  47485  elsprel  47637  clnbgrval  47984  dfvopnbgr2  48015  vopnbgrel  48016  dfclnbgr6  48018  dfnbgr6  48019  cycl3grtri  48109  dmmpossx2  48499  lindslinindsimp2  48625  ldepspr  48635  ldepsnlinc  48670  line  48894  rrxline  48896  dftpos5  49035  tposideq  49049  initc  49252  setc2othin  49627  functermceu  49671  idfudiag1  49686  funcsn  49702  0fucterm  49704  mndtcval  49740  mndtcbas  49742