Theorem sneq 4532

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 2770	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2822	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4523	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4523	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2818	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1538  {cab 2735  {csn 4522

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-sn 4523

This theorem is referenced by:  sneqi  4533  sneqd  4534  euabsn  4619  absneu  4621  preq1  4626  tpeq3  4637  issn  4720  mosneq  4730  sneqbg  4731  opeq1  4761  opeq1OLD  4762  propeqop  5366  opthwiener  5373  otiunsndisj  5379  opeliunxp  5588  relop  5690  elimasng  5927  inisegn0  5933  xpdifid  5997  dmsnsnsn  6049  predeq123  6127  suceq  6234  iotajust  6293  fconstg  6551  f1osng  6642  opabiotafun  6733  fvn0ssdmfun  6833  fsng  6890  fsn2g  6891  fnressn  6911  fressnfv  6913  funfvima3  6990  f12dfv  7022  f13dfv  7023  isofrlem  7087  isoselem  7088  elxp4  7632  elxp5  7633  1stval  7695  2ndval  7696  2ndval2  7711  fo1st  7713  fo2nd  7714  f1stres  7717  f2ndres  7718  mpomptsx  7766  dmmpossx  7768  fmpox  7769  ovmptss  7793  fparlem3  7814  fparlem4  7815  suppval  7837  suppsnop  7852  ressuppssdif  7859  brtpos2  7908  dftpos4  7921  tpostpos  7922  eceq1  8337  fvdiagfn  8473  mapsncnv  8475  elixpsn  8519  ixpsnf1o  8520  ensn1g  8593  en1  8595  difsnen  8620  xpsneng  8623  xpcomco  8628  xpassen  8632  xpdom2  8633  canth2  8692  phplem3  8720  rexdif1en  8732  xpfi  8822  marypha2lem2  8933  cardsn  9431  pm54.43  9463  dfac5lem3  9585  dfac5lem4  9586  kmlem9  9618  kmlem11  9620  kmlem12  9621  ackbij1lem8  9687  r1om  9704  fictb  9705  hsmexlem4  9889  axcc2lem  9896  axcc2  9897  axdc3lem4  9913  fpwwe2cbv  10090  fpwwe2lem3  10093  fpwwecbv  10104  canth4  10107  s3iunsndisj  14375  fsum2dlem  15173  fsumcnv  15176  fsumcom2  15177  ackbijnn  15231  fprod2dlem  15382  fprodcnv  15385  fprodcom2  15386  lcmfunsnlem1  16033  lcmfunsnlem2lem1  16034  lcmfunsnlem2lem2  16035  lcmfunsnlem2  16036  lcmfunsn  16040  vdwlem1  16372  vdwlem12  16383  vdwlem13  16384  vdwnn  16389  0ram  16411  ramz2  16415  pwsval  16817  symg2bas  18588  symgfixelsi  18630  pmtrfv  18647  pmtrprfval  18682  sylow2a  18811  efgrelexlema  18942  gsum2dlem2  19159  gsum2d2  19162  gsumcom2  19163  dprdcntz  19198  dprddisj  19199  dprd2dlem2  19230  dprd2dlem1  19231  dprd2da  19232  ablfac1eu  19263  ablfaclem3  19277  lssats2  19840  lspsneq0  19852  lbsind  19920  lspsneq  19962  lspdisj2  19967  lspsnsubn0  19980  lspprat  19993  islbs2  19994  lbsextlem4  20001  lbsextg  20002  lpi0  20088  lpi1  20089  frlmlbs  20562  lindfind  20581  lindsind  20582  lindfrn  20586  psrvsca  20719  evlssca  20852  mpfind  20870  coe1fv  20930  coe1tm  20997  pf1ind  21074  submaval  21281  mdetunilem3  21314  mdetunilem4  21315  mdetunilem9  21320  islp  21840  perfi  21855  t1sncld  22026  bwth  22110  dis2ndc  22160  nllyi  22175  dissnlocfin  22229  ptbasfi  22281  txkgen  22352  xkofvcn  22384  xkoinjcn  22387  qtopeu  22416  txswaphmeolem  22504  pt1hmeo  22506  elflim2  22664  cnextfvval  22765  cnextcn  22767  cnextfres1  22768  cnextfres  22769  tsmsxplem1  22853  tsmsxplem2  22854  ucncn  22986  itg11  24391  i1faddlem  24393  i1fmullem  24394  itg1addlem3  24398  itg1mulc  24404  eldv  24597  ply1lpir  24878  areambl  25643  tglngval  26444  edglnl  27035  nbgrval  27225  nbgr2vtx1edg  27239  nbuhgr2vtx1edgb  27241  nbgr1vtx  27247  nb3grprlem2  27270  uvtxel  27277  uvtxel1  27285  uvtxusgrel  27292  cusgredg  27313  cplgr1v  27319  cplgr3v  27324  usgredgsscusgredg  27348  vtxdgval  27357  1loopgrvd2  27392  wlk1walk  27527  wlkres  27559  wlkp1lem8  27569  usgr2pthlem  27651  crctcshwlkn0lem6  27700  2wspiundisj  27848  clwwlknon1  27981  1wlkdlem4  28024  eupth2lem3lem3  28114  frcond1  28150  frgr1v  28155  nfrgr2v  28156  frgr3v  28159  1vwmgr  28160  3vfriswmgr  28162  3cyclfrgrrn1  28169  n4cyclfrgr  28175  frgrwopreglem4a  28194  h1de2ctlem  29437  spansn  29441  elspansn  29448  elspansn2  29449  spansneleq  29452  h1datom  29464  spansnj  29529  spansncv  29535  superpos  30236  sumdmdlem2  30301  aciunf1lem  30523  fnpreimac  30532  dfcnv2  30537  pwrssmgc  30804  gsummpt2co  30834  gsumpart  30841  0nellinds  31087  lindssn  31094  lsmsnidl  31108  nsgmgclem  31117  nsgmgc  31118  nsgqusf1olem1  31119  nsgqusf1olem2  31120  nsgqusf1olem3  31121  elrspunidl  31127  lbslsat  31220  lindsunlem  31226  extdgval  31250  locfinreflem  31311  esum2dlem  31579  sibfima  31824  sibfof  31826  bnj1373  32530  bnj1489  32556  funen1cnv  32585  cplgredgex  32598  pfxwlk  32601  revwlk  32602  loop1cycl  32615  cvmscbv  32736  cvmsdisj  32748  cvmsss2  32752  cvmliftlem15  32776  cvmlift2lem11  32791  cvmlift2lem12  32792  cvmlift2lem13  32793  satffunlem1lem1  32880  satffunlem2lem1  32882  mvtinf  33033  eldm3  33244  elima4  33266  xpord2pred  33347  xpord3pred  33353  conway  33556  scutval  33557  scutcut  33558  scutbday  33559  eqscut  33560  eqscut2  33561  scutun12  33565  scutbdaybnd  33570  scutbdaybnd2  33571  scutbdaylt  33573  bday1s  33585  madebdaylemlrcut  33636  fvsingle  33771  snelsingles  33773  dfiota3  33774  brapply  33789  funpartlem  33793  altopeq12  33813  ranksng  34018  neibastop3  34100  tailval  34111  filnetlem4  34119  bj-restsnss  34778  bj-restsnss2  34779  f1omptsnlem  35033  f1omptsn  35034  mptsnun  35036  dissneqlem  35037  dissneq  35038  fvineqsnf1  35107  lindsadd  35330  lindsenlbs  35332  poimirlem4  35341  poimirlem25  35362  poimirlem26  35363  poimirlem27  35364  poimirlem31  35368  poimirlem32  35369  heiborlem3  35531  ismrer1  35556  lshpnel2N  36561  lsatlspsn2  36568  lsatlspsn  36569  lsatspn0  36576  lkrscss  36674  lfl1dim  36697  lfl1dim2N  36698  ldualvs  36713  atpointN  37319  watvalN  37569  trnsetN  37732  dih1dimatlem  38905  dihatexv  38914  dihjat1lem  39004  dihjat1  39005  lcfl7N  39077  lcfl8  39078  lcfl9a  39081  lcfrlem8  39125  lcfrlem9  39126  lcf1o  39127  mapdval2N  39206  mapdval4N  39208  mapdspex  39244  mapdn0  39245  mapdpglem23  39270  mapdpg  39282  mapdindp1  39296  mapdheq  39304  hvmapval  39336  mapdh9a  39365  hdmap1eq  39377  hdmap1cbv  39378  hdmapval  39404  hdmap10  39416  hdmaplkr  39489  evlsbagval  39780  0prjspnrel  39961  mzpclval  40039  mzpcl1  40043  wopprc  40344  dnnumch3lem  40363  aomclem8  40378  mendvsca  40508  cytpval  40526  snen1g  40605  k0004lem3  41225  dvconstbi  41411  wessf1ornlem  42181  dvmptfprodlem  42952  fourierdlem32  43147  fourierdlem33  43148  fourierdlem48  43162  funressnmo  44004  aiotajust  44007  funressndmafv2rn  44147  fzopredsuc  44248  elsprel  44360  irinitoringc  45060  opeliun2xp  45101  dmmpossx2  45105  lindslinindsimp2  45237  ldepspr  45247  ldepsnlinc  45282  line  45511  rrxline  45513