Theorem sneq 4568

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 2750	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2808	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4559	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4559	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2804	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1539  {cab 2715  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-sn 4559

This theorem is referenced by:  sneqi  4569  sneqd  4570  euabsn  4659  absneu  4661  preq1  4666  tpeq3  4677  issn  4760  mosneq  4770  sneqbg  4771  opeq1  4801  propeqop  5415  opthwiener  5422  otiunsndisj  5428  opeliunxp  5645  relop  5748  elimasngOLD  5987  inisegn0  5995  xpdifid  6060  dmsnsnsn  6112  predeq123  6192  suceq  6316  iotajust  6375  fconstg  6645  f1osng  6740  opabiotafun  6831  fvn0ssdmfun  6934  fsng  6991  fsn2g  6992  fnressn  7012  fressnfv  7014  funfvima3  7094  f12dfv  7126  f13dfv  7127  isofrlem  7191  isoselem  7192  elxp4  7743  elxp5  7744  1stval  7806  2ndval  7807  2ndval2  7822  fo1st  7824  fo2nd  7825  f1stres  7828  f2ndres  7829  mpomptsx  7877  dmmpossx  7879  fmpox  7880  ovmptss  7904  fparlem3  7925  fparlem4  7926  suppval  7950  suppsnop  7965  ressuppssdif  7972  brtpos2  8019  dftpos4  8032  tpostpos  8033  eceq1  8494  fvdiagfn  8637  mapsncnv  8639  elixpsn  8683  ixpsnf1o  8684  ensn1g  8763  en1  8765  en1OLD  8766  difsnen  8794  xpsneng  8797  xpcomco  8802  xpassen  8806  xpdom2  8807  canth2  8866  phplem3  8894  rexdif1en  8906  cnvfi  8924  xpfi  9015  marypha2lem2  9125  cardsn  9658  pm54.43  9690  dfac5lem3  9812  dfac5lem4  9813  kmlem9  9845  kmlem11  9847  kmlem12  9848  ackbij1lem8  9914  r1om  9931  fictb  9932  hsmexlem4  10116  axcc2lem  10123  axcc2  10124  axdc3lem4  10140  fpwwe2cbv  10317  fpwwe2lem3  10320  fpwwecbv  10331  canth4  10334  s3iunsndisj  14607  fsum2dlem  15410  fsumcnv  15413  fsumcom2  15414  ackbijnn  15468  fprod2dlem  15618  fprodcnv  15621  fprodcom2  15622  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  lcmfunsnlem2  16273  lcmfunsn  16277  vdwlem1  16610  vdwlem12  16621  vdwlem13  16622  vdwnn  16627  0ram  16649  ramz2  16653  pwsval  17114  symg2bas  18915  symgfixelsi  18958  pmtrfv  18975  pmtrprfval  19010  sylow2a  19139  efgrelexlema  19270  gsum2dlem2  19487  gsum2d2  19490  gsumcom2  19491  dprdcntz  19526  dprddisj  19527  dprd2dlem2  19558  dprd2dlem1  19559  dprd2da  19560  ablfac1eu  19591  ablfaclem3  19605  lssats2  20177  lspsneq0  20189  lbsind  20257  lspsneq  20299  lspdisj2  20304  lspsnsubn0  20317  lspprat  20330  islbs2  20331  lbsextlem4  20338  lbsextg  20339  lpi0  20431  lpi1  20432  frlmlbs  20914  lindfind  20933  lindsind  20934  lindfrn  20938  psrvsca  21070  evlssca  21209  mpfind  21227  coe1fv  21287  coe1tm  21354  pf1ind  21431  submaval  21638  mdetunilem3  21671  mdetunilem4  21672  mdetunilem9  21677  islp  22199  perfi  22214  t1sncld  22385  bwth  22469  dis2ndc  22519  nllyi  22534  dissnlocfin  22588  ptbasfi  22640  txkgen  22711  xkofvcn  22743  xkoinjcn  22746  qtopeu  22775  txswaphmeolem  22863  pt1hmeo  22865  elflim2  23023  cnextfvval  23124  cnextcn  23126  cnextfres1  23127  cnextfres  23128  tsmsxplem1  23212  tsmsxplem2  23213  ucncn  23345  itg11  24760  i1faddlem  24762  i1fmullem  24763  itg1addlem3  24767  itg1mulc  24774  eldv  24967  ply1lpir  25248  areambl  26013  tglngval  26816  edglnl  27416  nbgrval  27606  nbgr2vtx1edg  27620  nbuhgr2vtx1edgb  27622  nbgr1vtx  27628  nb3grprlem2  27651  uvtxel  27658  uvtxel1  27666  uvtxusgrel  27673  cusgredg  27694  cplgr1v  27700  cplgr3v  27705  usgredgsscusgredg  27729  vtxdgval  27738  1loopgrvd2  27773  wlk1walk  27908  wlkres  27940  wlkp1lem8  27950  usgr2pthlem  28032  crctcshwlkn0lem6  28081  2wspiundisj  28229  clwwlknon1  28362  1wlkdlem4  28405  eupth2lem3lem3  28495  frcond1  28531  frgr1v  28536  nfrgr2v  28537  frgr3v  28540  1vwmgr  28541  3vfriswmgr  28543  3cyclfrgrrn1  28550  n4cyclfrgr  28556  frgrwopreglem4a  28575  h1de2ctlem  29818  spansn  29822  elspansn  29829  elspansn2  29830  spansneleq  29833  h1datom  29845  spansnj  29910  spansncv  29916  superpos  30617  sumdmdlem2  30682  aciunf1lem  30901  fnpreimac  30910  dfcnv2  30915  pwrssmgc  31180  gsummpt2co  31210  gsumpart  31217  0nellinds  31468  lindssn  31475  lsmsnidl  31489  nsgmgclem  31498  nsgmgc  31499  nsgqusf1olem1  31500  nsgqusf1olem2  31501  nsgqusf1olem3  31502  elrspunidl  31508  lbslsat  31601  lindsunlem  31607  extdgval  31631  locfinreflem  31692  esum2dlem  31960  sibfima  32205  sibfof  32207  bnj1373  32910  bnj1489  32936  funen1cnv  32960  fineqvac  32966  cplgredgex  32982  pfxwlk  32985  revwlk  32986  loop1cycl  32999  cvmscbv  33120  cvmsdisj  33132  cvmsss2  33136  cvmliftlem15  33160  cvmlift2lem11  33175  cvmlift2lem12  33176  cvmlift2lem13  33177  satffunlem1lem1  33264  satffunlem2lem1  33266  mvtinf  33417  eldm3  33634  elima4  33656  xpord2pred  33719  xpord3pred  33725  naddcllem  33758  conway  33920  scutval  33921  scutcut  33922  scutbday  33925  eqscut  33926  eqscut2  33927  scutun12  33931  scutbdaybnd  33936  scutbdaybnd2  33937  scutbdaylt  33939  bday1s  33952  madebdaylemlrcut  34006  cofcut1  34017  cofcutr  34019  fvsingle  34149  snelsingles  34151  dfiota3  34152  brapply  34167  funpartlem  34171  altopeq12  34191  ranksng  34396  neibastop3  34478  tailval  34489  filnetlem4  34497  bj-restsnss  35181  bj-restsnss2  35182  f1omptsnlem  35434  f1omptsn  35435  mptsnun  35437  dissneqlem  35438  dissneq  35439  fvineqsnf1  35508  lindsadd  35697  lindsenlbs  35699  poimirlem4  35708  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem31  35735  poimirlem32  35736  heiborlem3  35898  ismrer1  35923  lshpnel2N  36926  lsatlspsn2  36933  lsatlspsn  36934  lsatspn0  36941  lkrscss  37039  lfl1dim  37062  lfl1dim2N  37063  ldualvs  37078  atpointN  37684  watvalN  37934  trnsetN  38097  dih1dimatlem  39270  dihatexv  39279  dihjat1lem  39369  dihjat1  39370  lcfl7N  39442  lcfl8  39443  lcfl9a  39446  lcfrlem8  39490  lcfrlem9  39491  lcf1o  39492  mapdval2N  39571  mapdval4N  39573  mapdspex  39609  mapdn0  39610  mapdpglem23  39635  mapdpg  39647  mapdindp1  39661  mapdheq  39669  hvmapval  39701  mapdh9a  39730  hdmap1eq  39742  hdmap1cbv  39743  hdmapval  39769  hdmap10  39781  hdmaplkr  39854  sn-iotalem  40117  sn-iotanul  40121  evlsbagval  40198  0prjspnrel  40385  mzpclval  40463  mzpcl1  40467  wopprc  40768  dnnumch3lem  40787  aomclem8  40802  mendvsca  40932  cytpval  40950  snen1g  41029  k0004lem3  41648  dvconstbi  41841  wessf1ornlem  42611  dvmptfprodlem  43375  fourierdlem32  43570  fourierdlem33  43571  fourierdlem48  43585  funressnmo  44427  aiotajust  44463  funressndmafv2rn  44602  fzopredsuc  44703  elsprel  44815  irinitoringc  45515  opeliun2xp  45556  dmmpossx2  45560  lindslinindsimp2  45692  ldepspr  45702  ldepsnlinc  45737  line  45966  rrxline  45968  setc2othin  46225  mndtcval  46252  mndtcbas  46254