Theorem sneq 4592

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 2749	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2803	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4583	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4583	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1542  {cab 2715  {csn 4582

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-sn 4583

This theorem is referenced by:  sneqi  4593  sneqd  4594  euabsn  4685  absneu  4687  preq1  4692  tpeq3  4703  issn  4790  mosneq  4800  sneqbg  4801  opeq1  4831  snexgALT  5387  propeqop  5463  opthwiener  5470  otiunsndisj  5476  opeliunxp  5699  opeliun2xp  5700  relop  5807  inisegn0  6065  xpdifid  6134  dmsnsnsn  6186  predeq123  6268  iotajust  6455  iotanul2  6473  fconstg  6729  f1osng  6824  opabiotafun  6922  fvn0ssdmfun  7028  fsng  7092  fsn2g  7093  fnressn  7113  fressnfv  7115  funfvima3  7192  f12dfv  7229  f13dfv  7230  isofrlem  7296  isoselem  7297  elxp4  7874  elxp5  7875  1stval  7945  2ndval  7946  2ndval2  7961  fo1st  7963  fo2nd  7964  f1stres  7967  f2ndres  7968  mpomptsx  8018  dmmpossx  8020  fmpox  8021  ovmptss  8045  fparlem3  8066  fparlem4  8067  xpord2pred  8097  xpord3pred  8104  suppval  8114  suppsnop  8130  ressuppssdif  8137  brtpos2  8184  dftpos4  8197  tpostpos  8198  naddcllem  8614  eceq1  8685  fvdiagfn  8841  mapsncnv  8843  elixpsn  8887  ixpsnf1o  8888  ensn1g  8971  en1  8973  difsnen  8999  xpsneng  9002  xpcomco  9007  xpassen  9011  xpdom2  9012  canth2  9070  rexdif1en  9097  cnvfi  9112  marypha2lem2  9351  cardsn  9893  pm54.43  9925  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem9  10081  kmlem11  10083  kmlem12  10084  ackbij1lem8  10148  r1om  10165  fictb  10166  hsmexlem4  10351  axcc2lem  10358  axcc2  10359  axdc3lem4  10375  fpwwe2cbv  10553  fpwwe2lem3  10556  fpwwecbv  10567  canth4  10570  s3iunsndisj  14903  fsum2dlem  15705  fsumcnv  15708  fsumcom2  15709  ackbijnn  15763  fprod2dlem  15915  fprodcnv  15918  fprodcom2  15919  lcmfunsnlem1  16576  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  lcmfunsn  16583  vdwlem1  16921  vdwlem12  16932  vdwlem13  16933  vdwnn  16938  0ram  16960  ramz2  16964  pwsval  17418  symg2bas  19334  symgfixelsi  19376  pmtrfv  19393  pmtrprfval  19428  sylow2a  19560  efgrelexlema  19690  gsum2dlem2  19912  gsum2d2  19915  gsumcom2  19916  dprdcntz  19951  dprddisj  19952  dprd2dlem2  19983  dprd2dlem1  19984  dprd2da  19985  ablfac1eu  20016  ablfaclem3  20030  lssats2  20963  lspsneq0  20975  lbsind  21044  lspsneq  21089  lspdisj2  21094  lspsnsubn0  21107  lspprat  21120  islbs2  21121  lbsextlem4  21128  lbsextg  21129  lpi0  21293  lpi1  21294  irinitoringc  21446  pzriprnglem13  21460  pzriprnglem14  21461  frlmlbs  21764  lindfind  21783  lindsind  21784  lindfrn  21788  psrvsca  21917  evlsvvval  22060  evlssca  22061  mpfind  22082  coe1fv  22159  coe1tm  22227  pf1ind  22311  submaval  22537  mdetunilem3  22570  mdetunilem4  22571  mdetunilem9  22576  islp  23096  perfi  23111  t1sncld  23282  bwth  23366  dis2ndc  23416  nllyi  23431  dissnlocfin  23485  ptbasfi  23537  txkgen  23608  xkofvcn  23640  xkoinjcn  23643  qtopeu  23672  txswaphmeolem  23760  pt1hmeo  23762  elflim2  23920  cnextfvval  24021  cnextcn  24023  cnextfres1  24024  cnextfres  24025  tsmsxplem1  24109  tsmsxplem2  24110  ucncn  24240  itg11  25660  i1faddlem  25662  i1fmullem  25663  itg1addlem3  25667  itg1mulc  25673  eldv  25867  ply1lpir  26155  areambl  26936  conway  27787  cutsval  27788  cutcuts  27789  cutbday  27792  eqcuts  27793  eqcuts2  27794  cutsun12  27798  cutbdaybnd  27803  cutbdaybnd2  27804  cutbdaylt  27806  eqcuts3  27812  bday1  27822  cuteq0  27823  cuteq1  27825  madebdaylemlrcut  27907  sltsbday  27925  cofcut1  27928  cofcutr  27932  oniso  28279  bdayn0p1  28377  expsval  28433  pw2cut2  28470  tglngval  28635  edglnl  29228  nbgrval  29421  nbgr2vtx1edg  29435  nbuhgr2vtx1edgb  29437  nbgr1vtx  29443  nb3grprlem2  29466  uvtxel  29473  uvtxel1  29481  uvtxusgrel  29488  cusgredg  29509  cplgr1v  29515  cplgr3v  29520  usgredgsscusgredg  29545  vtxdgval  29554  1loopgrvd2  29589  wlk1walk  29724  wlkres  29754  wlkp1lem8  29764  usgr2pthlem  29848  crctcshwlkn0lem6  29900  2wspiundisj  30051  clwwlknon1  30184  1wlkdlem4  30227  eupth2lem3lem3  30317  frcond1  30353  frgr1v  30358  nfrgr2v  30359  frgr3v  30362  1vwmgr  30363  3vfriswmgr  30365  3cyclfrgrrn1  30372  n4cyclfrgr  30378  frgrwopreglem4a  30397  h1de2ctlem  31643  spansn  31647  elspansn  31654  elspansn2  31655  spansneleq  31658  h1datom  31670  spansnj  31735  spansncv  31741  superpos  32442  sumdmdlem2  32507  aciunf1lem  32752  fnpreimac  32760  dfcnv2  32765  pwrssmgc  33093  gsummpt2co  33142  gsumpart  33157  gsumwrd2dccatlem  33171  gsumwrd2dccat  33172  0nellinds  33463  lindssn  33471  lsmsnidl  33492  nsgmgclem  33504  nsgmgc  33505  nsgqusf1olem1  33506  nsgqusf1olem2  33507  nsgqusf1olem3  33508  pidlnzb  33515  elrspunidl  33521  extvfval  33709  esplyfval1  33750  esplyfvaln  33751  lbslsat  33794  lindsunlem  33802  extdgval  33831  fldextrspunlsplem  33851  locfinreflem  34018  esum2dlem  34270  sibfima  34516  sibfof  34518  bnj1373  35206  bnj1489  35232  funen1cnv  35265  fineqvac  35294  cplgredgex  35337  pfxwlk  35340  revwlk  35341  loop1cycl  35353  cvmscbv  35474  cvmsdisj  35486  cvmsss2  35490  cvmliftlem15  35514  cvmlift2lem11  35529  cvmlift2lem12  35530  cvmlift2lem13  35531  satffunlem1lem1  35618  satffunlem2lem1  35620  mvtinf  35771  eldm3  35977  elima4  35992  fvsingle  36134  snelsingles  36136  dfiota3  36137  brapply  36152  funpartlem  36158  altopeq12  36178  ranksng  36383  neibastop3  36578  tailval  36589  filnetlem4  36597  bj-snexg  37282  bj-restsnss  37336  bj-restsnss2  37337  f1omptsnlem  37591  f1omptsn  37592  mptsnun  37594  dissneqlem  37595  dissneq  37596  fvineqsnf1  37665  lindsadd  37864  lindsenlbs  37866  poimirlem4  37875  poimirlem25  37896  poimirlem26  37897  poimirlem27  37898  poimirlem31  37902  poimirlem32  37903  heiborlem3  38064  ismrer1  38089  lshpnel2N  39361  lsatlspsn2  39368  lsatlspsn  39369  lsatspn0  39376  lkrscss  39474  lfl1dim  39497  lfl1dim2N  39498  ldualvs  39513  atpointN  40119  watvalN  40369  trnsetN  40532  dih1dimatlem  41705  dihatexv  41714  dihjat1lem  41804  dihjat1  41805  lcfl7N  41877  lcfl8  41878  lcfl9a  41881  lcfrlem8  41925  lcfrlem9  41926  lcf1o  41927  mapdval2N  42006  mapdval4N  42008  mapdspex  42044  mapdn0  42045  mapdpglem23  42070  mapdpg  42082  mapdindp1  42096  mapdheq  42104  hvmapval  42136  mapdh9a  42165  hdmap1eq  42177  hdmap1cbv  42178  hdmapval  42204  hdmap10  42216  hdmaplkr  42289  sn-iotalem  42593  evlsevl  42932  0prjspnrel  42985  mzpclval  43082  mzpcl1  43086  wopprc  43387  dnnumch3lem  43403  aomclem8  43418  mendvsca  43544  cytpval  43559  snen1g  43880  k0004lem3  44505  dvconstbi  44690  relpfrlem  45309  permaxinf2lem  45368  wessf1ornlem  45544  dvmptfprodlem  46302  fourierdlem32  46497  fourierdlem33  46498  fourierdlem48  46512  funressnmo  47406  aiotajust  47444  funressndmafv2rn  47583  fzopredsuc  47683  elsprel  47835  clnbgrval  48182  dfvopnbgr2  48213  vopnbgrel  48214  dfclnbgr6  48216  dfnbgr6  48217  cycl3grtri  48307  dmmpossx2  48697  lindslinindsimp2  48823  ldepspr  48833  ldepsnlinc  48868  line  49092  rrxline  49094  dftpos5  49233  tposideq  49247  initc  49450  setc2othin  49825  functermceu  49869  idfudiag1  49884  funcsn  49900  0fucterm  49902  mndtcval  49938  mndtcbas  49940