Theorem sneq 4640

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

Syntax hints:   → wi 4   = wceq 1536  {cab 2711  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-sn 4631

This theorem is referenced by:  sneqi  4641  sneqd  4642  euabsn  4730  absneu  4732  preq1  4737  tpeq3  4748  issn  4836  mosneq  4846  sneqbg  4847  opeq1  4877  snexg  5440  propeqop  5516  opthwiener  5523  otiunsndisj  5529  opeliunxp  5755  relop  5863  elimasngOLD  6110  inisegn0  6118  xpdifid  6189  dmsnsnsn  6241  predeq123  6323  suceq  6451  iotajust  6514  iotanul2  6532  fconstg  6795  f1osng  6889  opabiotafun  6988  fvn0ssdmfun  7093  fsng  7156  fsn2g  7157  fnressn  7177  fressnfv  7179  funfvima3  7255  f12dfv  7292  f13dfv  7293  isofrlem  7359  isoselem  7360  elxp4  7944  elxp5  7945  1stval  8014  2ndval  8015  2ndval2  8030  fo1st  8032  fo2nd  8033  f1stres  8036  f2ndres  8037  mpomptsx  8087  dmmpossx  8089  fmpox  8090  ovmptss  8116  fparlem3  8137  fparlem4  8138  xpord2pred  8168  xpord3pred  8175  suppval  8185  suppsnop  8201  ressuppssdif  8208  brtpos2  8255  dftpos4  8268  tpostpos  8269  naddcllem  8712  eceq1  8782  fvdiagfn  8929  mapsncnv  8931  elixpsn  8975  ixpsnf1o  8976  ensn1g  9060  en1  9062  difsnen  9091  xpsneng  9094  xpcomco  9100  xpassen  9104  xpdom2  9105  canth2  9168  rexdif1en  9196  rexdif1enOLD  9197  cnvfi  9214  phplem3OLD  9253  xpfiOLD  9356  marypha2lem2  9473  cardsn  10006  pm54.43  10038  dfac5lem3  10162  dfac5lem4  10163  dfac5lem4OLD  10165  kmlem9  10196  kmlem11  10198  kmlem12  10199  ackbij1lem8  10263  r1om  10280  fictb  10281  hsmexlem4  10466  axcc2lem  10473  axcc2  10474  axdc3lem4  10490  fpwwe2cbv  10667  fpwwe2lem3  10670  fpwwecbv  10681  canth4  10684  s3iunsndisj  15003  fsum2dlem  15802  fsumcnv  15805  fsumcom2  15806  ackbijnn  15860  fprod2dlem  16012  fprodcnv  16015  fprodcom2  16016  lcmfunsnlem1  16670  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfunsnlem2  16673  lcmfunsn  16677  vdwlem1  17014  vdwlem12  17025  vdwlem13  17026  vdwnn  17031  0ram  17053  ramz2  17057  pwsval  17532  symg2bas  19424  symgfixelsi  19467  pmtrfv  19484  pmtrprfval  19519  sylow2a  19651  efgrelexlema  19781  gsum2dlem2  20003  gsum2d2  20006  gsumcom2  20007  dprdcntz  20042  dprddisj  20043  dprd2dlem2  20074  dprd2dlem1  20075  dprd2da  20076  ablfac1eu  20107  ablfaclem3  20121  lssats2  21015  lspsneq0  21027  lbsind  21096  lspsneq  21141  lspdisj2  21146  lspsnsubn0  21159  lspprat  21172  islbs2  21173  lbsextlem4  21180  lbsextg  21181  lpi0  21353  lpi1  21354  irinitoringc  21507  pzriprnglem13  21521  pzriprnglem14  21522  frlmlbs  21834  lindfind  21853  lindsind  21854  lindfrn  21858  psrvsca  21986  evlssca  22130  mpfind  22148  coe1fv  22223  coe1tm  22291  pf1ind  22374  submaval  22602  mdetunilem3  22635  mdetunilem4  22636  mdetunilem9  22641  islp  23163  perfi  23178  t1sncld  23349  bwth  23433  dis2ndc  23483  nllyi  23498  dissnlocfin  23552  ptbasfi  23604  txkgen  23675  xkofvcn  23707  xkoinjcn  23710  qtopeu  23739  txswaphmeolem  23827  pt1hmeo  23829  elflim2  23987  cnextfvval  24088  cnextcn  24090  cnextfres1  24091  cnextfres  24092  tsmsxplem1  24176  tsmsxplem2  24177  ucncn  24309  itg11  25739  i1faddlem  25741  i1fmullem  25742  itg1addlem3  25746  itg1mulc  25753  eldv  25947  ply1lpir  26235  areambl  27015  conway  27858  scutval  27859  scutcut  27860  scutbday  27863  eqscut  27864  eqscut2  27865  scutun12  27869  scutbdaybnd  27874  scutbdaybnd2  27875  scutbdaylt  27877  bday1s  27890  cuteq0  27891  cuteq1  27892  madebdaylemlrcut  27951  cofcut1  27968  cofcutr  27972  expsval  28422  tglngval  28573  edglnl  29174  nbgrval  29367  nbgr2vtx1edg  29381  nbuhgr2vtx1edgb  29383  nbgr1vtx  29389  nb3grprlem2  29412  uvtxel  29419  uvtxel1  29427  uvtxusgrel  29434  cusgredg  29455  cplgr1v  29461  cplgr3v  29466  usgredgsscusgredg  29491  vtxdgval  29500  1loopgrvd2  29535  wlk1walk  29671  wlkres  29702  wlkp1lem8  29712  usgr2pthlem  29795  crctcshwlkn0lem6  29844  2wspiundisj  29992  clwwlknon1  30125  1wlkdlem4  30168  eupth2lem3lem3  30258  frcond1  30294  frgr1v  30299  nfrgr2v  30300  frgr3v  30303  1vwmgr  30304  3vfriswmgr  30306  3cyclfrgrrn1  30313  n4cyclfrgr  30319  frgrwopreglem4a  30338  h1de2ctlem  31583  spansn  31587  elspansn  31594  elspansn2  31595  spansneleq  31598  h1datom  31610  spansnj  31675  spansncv  31681  superpos  32382  sumdmdlem2  32447  aciunf1lem  32678  fnpreimac  32687  dfcnv2  32692  pwrssmgc  32974  gsummpt2co  33033  gsumpart  33042  gsumwrd2dccatlem  33051  gsumwrd2dccat  33052  0nellinds  33377  lindssn  33385  lsmsnidl  33406  nsgmgclem  33418  nsgmgc  33419  nsgqusf1olem1  33420  nsgqusf1olem2  33421  nsgqusf1olem3  33422  pidlnzb  33429  elrspunidl  33435  lbslsat  33643  lindsunlem  33651  extdgval  33681  locfinreflem  33800  esum2dlem  34072  sibfima  34319  sibfof  34321  bnj1373  35022  bnj1489  35048  funen1cnv  35080  fineqvac  35089  cplgredgex  35104  pfxwlk  35107  revwlk  35108  loop1cycl  35121  cvmscbv  35242  cvmsdisj  35254  cvmsss2  35258  cvmliftlem15  35282  cvmlift2lem11  35297  cvmlift2lem12  35298  cvmlift2lem13  35299  satffunlem1lem1  35386  satffunlem2lem1  35388  mvtinf  35539  eldm3  35740  elima4  35756  fvsingle  35901  snelsingles  35903  dfiota3  35904  brapply  35919  funpartlem  35923  altopeq12  35943  ranksng  36148  neibastop3  36344  tailval  36355  filnetlem4  36363  bj-snexg  37016  bj-restsnss  37065  bj-restsnss2  37066  f1omptsnlem  37318  f1omptsn  37319  mptsnun  37321  dissneqlem  37322  dissneq  37323  fvineqsnf1  37392  lindsadd  37599  lindsenlbs  37601  poimirlem4  37610  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem31  37637  poimirlem32  37638  heiborlem3  37799  ismrer1  37824  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  42238  evlsvvval  42549  evlsevl  42557  0prjspnrel  42613  mzpclval  42712  mzpcl1  42716  wopprc  43018  dnnumch3lem  43034  aomclem8  43049  mendvsca  43175  cytpval  43190  snen1g  43513  k0004lem3  44138  dvconstbi  44329  wessf1ornlem  45127  dvmptfprodlem  45899  fourierdlem32  46094  fourierdlem33  46095  fourierdlem48  46109  funressnmo  46995  aiotajust  47033  funressndmafv2rn  47172  fzopredsuc  47272  elsprel  47399  clnbgrval  47746  dfvopnbgr2  47776  vopnbgrel  47777  dfclnbgr6  47779  dfnbgr6  47780  opeliun2xp  48177  dmmpossx2  48181  lindslinindsimp2  48308  ldepspr  48318  ldepsnlinc  48353  line  48581  rrxline  48583  setc2othin  48856  mndtcval  48887  mndtcbas  48889