Theorem sneq 4578

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

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

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 4569

This theorem is referenced by:  sneqi  4579  sneqd  4580  euabsn  4671  absneu  4673  preq1  4678  tpeq3  4689  issn  4776  mosneq  4786  sneqbg  4787  opeq1  4817  snexgALT  5376  propeqop  5453  opthwiener  5460  otiunsndisj  5466  opeliunxp  5689  opeliun2xp  5690  relop  5797  inisegn0  6055  xpdifid  6124  dmsnsnsn  6176  predeq123  6258  iotajust  6445  iotanul2  6463  fconstg  6719  f1osng  6814  opabiotafun  6912  fvn0ssdmfun  7018  fsng  7082  fsn2g  7083  fnressn  7103  fressnfv  7105  funfvima3  7182  f12dfv  7219  f13dfv  7220  isofrlem  7286  isoselem  7287  elxp4  7864  elxp5  7865  1stval  7935  2ndval  7936  2ndval2  7951  fo1st  7953  fo2nd  7954  f1stres  7957  f2ndres  7958  mpomptsx  8008  dmmpossx  8010  fmpox  8011  ovmptss  8034  fparlem3  8055  fparlem4  8056  xpord2pred  8086  xpord3pred  8093  suppval  8103  suppsnop  8119  ressuppssdif  8126  brtpos2  8173  dftpos4  8186  tpostpos  8187  naddcllem  8603  eceq1  8674  fvdiagfn  8830  mapsncnv  8832  elixpsn  8876  ixpsnf1o  8877  ensn1g  8960  en1  8962  difsnen  8988  xpsneng  8991  xpcomco  8996  xpassen  9000  xpdom2  9001  canth2  9059  rexdif1en  9086  cnvfi  9101  marypha2lem2  9340  cardsn  9882  pm54.43  9914  dfac5lem3  10036  dfac5lem4  10037  dfac5lem4OLD  10039  kmlem9  10070  kmlem11  10072  kmlem12  10073  ackbij1lem8  10137  r1om  10154  fictb  10155  hsmexlem4  10340  axcc2lem  10347  axcc2  10348  axdc3lem4  10364  fpwwe2cbv  10542  fpwwe2lem3  10545  fpwwecbv  10556  canth4  10559  s3iunsndisj  14919  fsum2dlem  15721  fsumcnv  15724  fsumcom2  15725  ackbijnn  15782  fprod2dlem  15934  fprodcnv  15937  fprodcom2  15938  lcmfunsnlem1  16595  lcmfunsnlem2lem1  16596  lcmfunsnlem2lem2  16597  lcmfunsnlem2  16598  lcmfunsn  16602  vdwlem1  16941  vdwlem12  16952  vdwlem13  16953  vdwnn  16958  0ram  16980  ramz2  16984  pwsval  17438  symg2bas  19357  symgfixelsi  19399  pmtrfv  19416  pmtrprfval  19451  sylow2a  19583  efgrelexlema  19713  gsum2dlem2  19935  gsum2d2  19938  gsumcom2  19939  dprdcntz  19974  dprddisj  19975  dprd2dlem2  20006  dprd2dlem1  20007  dprd2da  20008  ablfac1eu  20039  ablfaclem3  20053  lssats2  20984  lspsneq0  20996  lbsind  21065  lspsneq  21110  lspdisj2  21115  lspsnsubn0  21128  lspprat  21141  islbs2  21142  lbsextlem4  21149  lbsextg  21150  lpi0  21314  lpi1  21315  irinitoringc  21467  pzriprnglem13  21481  pzriprnglem14  21482  frlmlbs  21785  lindfind  21804  lindsind  21805  lindfrn  21809  psrvsca  21936  evlsvvval  22079  evlssca  22080  mpfind  22101  coe1fv  22178  coe1tm  22246  pf1ind  22328  submaval  22554  mdetunilem3  22587  mdetunilem4  22588  mdetunilem9  22593  islp  23113  perfi  23128  t1sncld  23299  bwth  23383  dis2ndc  23433  nllyi  23448  dissnlocfin  23502  ptbasfi  23554  txkgen  23625  xkofvcn  23657  xkoinjcn  23660  qtopeu  23689  txswaphmeolem  23777  pt1hmeo  23779  elflim2  23937  cnextfvval  24038  cnextcn  24040  cnextfres1  24041  cnextfres  24042  tsmsxplem1  24126  tsmsxplem2  24127  ucncn  24257  itg11  25666  i1faddlem  25668  i1fmullem  25669  itg1addlem3  25673  itg1mulc  25679  eldv  25873  ply1lpir  26155  areambl  26933  conway  27783  cutsval  27784  cutcuts  27785  cutbday  27788  eqcuts  27789  eqcuts2  27790  cutsun12  27794  cutbdaybnd  27799  cutbdaybnd2  27800  cutbdaylt  27802  eqcuts3  27808  bday1  27818  cuteq0  27819  cuteq1  27821  madebdaylemlrcut  27903  sltsbday  27921  cofcut1  27924  cofcutr  27928  oniso  28275  bdayn0p1  28373  expsval  28429  pw2cut2  28466  tglngval  28631  edglnl  29224  nbgrval  29417  nbgr2vtx1edg  29431  nbuhgr2vtx1edgb  29433  nbgr1vtx  29439  nb3grprlem2  29462  uvtxel  29469  uvtxel1  29477  uvtxusgrel  29484  cusgredg  29505  cplgr1v  29511  cplgr3v  29516  usgredgsscusgredg  29541  vtxdgval  29550  1loopgrvd2  29585  wlk1walk  29720  wlkres  29750  wlkp1lem8  29760  usgr2pthlem  29844  crctcshwlkn0lem6  29896  2wspiundisj  30047  clwwlknon1  30180  1wlkdlem4  30223  eupth2lem3lem3  30313  frcond1  30349  frgr1v  30354  nfrgr2v  30355  frgr3v  30358  1vwmgr  30359  3vfriswmgr  30361  3cyclfrgrrn1  30368  n4cyclfrgr  30374  frgrwopreglem4a  30393  h1de2ctlem  31639  spansn  31643  elspansn  31650  elspansn2  31651  spansneleq  31654  h1datom  31666  spansnj  31731  spansncv  31737  superpos  32438  sumdmdlem2  32503  aciunf1lem  32748  fnpreimac  32756  dfcnv2  32761  pwrssmgc  33073  gsummpt2co  33122  gsumpart  33137  gsumwrd2dccatlem  33151  gsumwrd2dccat  33152  0nellinds  33443  lindssn  33451  lsmsnidl  33472  nsgmgclem  33484  nsgmgc  33485  nsgqusf1olem1  33486  nsgqusf1olem2  33487  nsgqusf1olem3  33488  pidlnzb  33495  elrspunidl  33501  extvfval  33689  esplyfval1  33730  esplyfvaln  33731  lbslsat  33774  lindsunlem  33782  extdgval  33811  fldextrspunlsplem  33831  locfinreflem  33998  esum2dlem  34250  sibfima  34496  sibfof  34498  bnj1373  35186  bnj1489  35212  funen1cnv  35245  fineqvac  35274  cplgredgex  35317  pfxwlk  35320  revwlk  35321  loop1cycl  35333  cvmscbv  35454  cvmsdisj  35466  cvmsss2  35470  cvmliftlem15  35494  cvmlift2lem11  35509  cvmlift2lem12  35510  cvmlift2lem13  35511  satffunlem1lem1  35598  satffunlem2lem1  35600  mvtinf  35751  eldm3  35957  elima4  35972  fvsingle  36114  snelsingles  36116  dfiota3  36117  brapply  36132  funpartlem  36138  altopeq12  36158  ranksng  36363  neibastop3  36558  tailval  36569  filnetlem4  36577  ttcid  36688  bj-snexg  37347  bj-restsnss  37401  bj-restsnss2  37402  f1omptsnlem  37656  f1omptsn  37657  mptsnun  37659  dissneqlem  37660  dissneq  37661  fvineqsnf1  37730  lindsadd  37938  lindsenlbs  37940  poimirlem4  37949  poimirlem25  37970  poimirlem26  37971  poimirlem27  37972  poimirlem31  37976  poimirlem32  37977  heiborlem3  38138  ismrer1  38163  lshpnel2N  39435  lsatlspsn2  39442  lsatlspsn  39443  lsatspn0  39450  lkrscss  39548  lfl1dim  39571  lfl1dim2N  39572  ldualvs  39587  atpointN  40193  watvalN  40443  trnsetN  40606  dih1dimatlem  41779  dihatexv  41788  dihjat1lem  41878  dihjat1  41879  lcfl7N  41951  lcfl8  41952  lcfl9a  41955  lcfrlem8  41999  lcfrlem9  42000  lcf1o  42001  mapdval2N  42080  mapdval4N  42082  mapdspex  42118  mapdn0  42119  mapdpglem23  42144  mapdpg  42156  mapdindp1  42170  mapdheq  42178  hvmapval  42210  mapdh9a  42239  hdmap1eq  42251  hdmap1cbv  42252  hdmapval  42278  hdmap10  42290  hdmaplkr  42363  sn-iotalem  42666  evlsevl  43011  0prjspnrel  43064  mzpclval  43161  mzpcl1  43165  wopprc  43466  dnnumch3lem  43482  aomclem8  43497  mendvsca  43623  cytpval  43638  snen1g  43959  k0004lem3  44584  dvconstbi  44769  relpfrlem  45388  permaxinf2lem  45447  wessf1ornlem  45623  dvmptfprodlem  46380  fourierdlem32  46575  fourierdlem33  46576  fourierdlem48  46590  funressnmo  47496  aiotajust  47534  funressndmafv2rn  47673  fzopredsuc  47774  elsprel  47937  clnbgrval  48300  dfvopnbgr2  48331  vopnbgrel  48332  dfclnbgr6  48334  dfnbgr6  48335  cycl3grtri  48425  dmmpossx2  48815  lindslinindsimp2  48941  ldepspr  48951  ldepsnlinc  48986  line  49210  rrxline  49212  dftpos5  49351  tposideq  49365  initc  49568  setc2othin  49943  functermceu  49987  idfudiag1  50002  funcsn  50018  0fucterm  50020  mndtcval  50056  mndtcbas  50058