Theorem sneq 4577

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 2748	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2802	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4568	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4568	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1542  {cab 2714  {csn 4567

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-sn 4568

This theorem is referenced by:  sneqi  4578  sneqd  4579  euabsn  4670  absneu  4672  preq1  4677  tpeq3  4688  issn  4775  mosneq  4785  sneqbg  4786  opeq1  4816  snexgALT  5383  propeqop  5461  opthwiener  5468  otiunsndisj  5474  opeliunxp  5698  opeliun2xp  5699  relop  5805  inisegn0  6063  xpdifid  6132  dmsnsnsn  6184  predeq123  6266  iotajust  6453  iotanul2  6471  fconstg  6727  f1osng  6822  opabiotafun  6920  fvn0ssdmfun  7026  fsng  7090  fsn2g  7091  fnressn  7112  fressnfv  7114  funfvima3  7191  f12dfv  7228  f13dfv  7229  isofrlem  7295  isoselem  7296  elxp4  7873  elxp5  7874  1stval  7944  2ndval  7945  2ndval2  7960  fo1st  7962  fo2nd  7963  f1stres  7966  f2ndres  7967  mpomptsx  8017  dmmpossx  8019  fmpox  8020  ovmptss  8043  fparlem3  8064  fparlem4  8065  xpord2pred  8095  xpord3pred  8102  suppval  8112  suppsnop  8128  ressuppssdif  8135  brtpos2  8182  dftpos4  8195  tpostpos  8196  naddcllem  8612  eceq1  8683  fvdiagfn  8839  mapsncnv  8841  elixpsn  8885  ixpsnf1o  8886  ensn1g  8969  en1  8971  difsnen  8997  xpsneng  9000  xpcomco  9005  xpassen  9009  xpdom2  9010  canth2  9068  rexdif1en  9095  cnvfi  9110  marypha2lem2  9349  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  14930  fsum2dlem  15732  fsumcnv  15735  fsumcom2  15736  ackbijnn  15793  fprod2dlem  15945  fprodcnv  15948  fprodcom2  15949  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfunsnlem2  16609  lcmfunsn  16613  vdwlem1  16952  vdwlem12  16963  vdwlem13  16964  vdwnn  16969  0ram  16991  ramz2  16995  pwsval  17449  symg2bas  19368  symgfixelsi  19410  pmtrfv  19427  pmtrprfval  19462  sylow2a  19594  efgrelexlema  19724  gsum2dlem2  19946  gsum2d2  19949  gsumcom2  19950  dprdcntz  19985  dprddisj  19986  dprd2dlem2  20017  dprd2dlem1  20018  dprd2da  20019  ablfac1eu  20050  ablfaclem3  20064  lssats2  20995  lspsneq0  21007  lbsind  21075  lspsneq  21120  lspdisj2  21125  lspsnsubn0  21138  lspprat  21151  islbs2  21152  lbsextlem4  21159  lbsextg  21160  lpi0  21324  lpi1  21325  irinitoringc  21459  pzriprnglem13  21473  pzriprnglem14  21474  frlmlbs  21777  lindfind  21796  lindsind  21797  lindfrn  21801  psrvsca  21928  evlsvvval  22071  evlssca  22072  mpfind  22093  coe1fv  22170  coe1tm  22238  pf1ind  22320  submaval  22546  mdetunilem3  22579  mdetunilem4  22580  mdetunilem9  22585  islp  23105  perfi  23120  t1sncld  23291  bwth  23375  dis2ndc  23425  nllyi  23440  dissnlocfin  23494  ptbasfi  23546  txkgen  23617  xkofvcn  23649  xkoinjcn  23652  qtopeu  23681  txswaphmeolem  23769  pt1hmeo  23771  elflim2  23929  cnextfvval  24030  cnextcn  24032  cnextfres1  24033  cnextfres  24034  tsmsxplem1  24118  tsmsxplem2  24119  ucncn  24249  itg11  25658  i1faddlem  25660  i1fmullem  25661  itg1addlem3  25665  itg1mulc  25671  eldv  25865  ply1lpir  26147  areambl  26922  conway  27771  cutsval  27772  cutcuts  27773  cutbday  27776  eqcuts  27777  eqcuts2  27778  cutsun12  27782  cutbdaybnd  27787  cutbdaybnd2  27788  cutbdaylt  27790  eqcuts3  27796  bday1  27806  cuteq0  27807  cuteq1  27809  madebdaylemlrcut  27891  sltsbday  27909  cofcut1  27912  cofcutr  27916  oniso  28263  bdayn0p1  28361  expsval  28417  pw2cut2  28454  tglngval  28619  edglnl  29212  nbgrval  29405  nbgr2vtx1edg  29419  nbuhgr2vtx1edgb  29421  nbgr1vtx  29427  nb3grprlem2  29450  uvtxel  29457  uvtxel1  29465  uvtxusgrel  29472  cusgredg  29493  cplgr1v  29499  cplgr3v  29504  usgredgsscusgredg  29528  vtxdgval  29537  1loopgrvd2  29572  wlk1walk  29707  wlkres  29737  wlkp1lem8  29747  usgr2pthlem  29831  crctcshwlkn0lem6  29883  2wspiundisj  30034  clwwlknon1  30167  1wlkdlem4  30210  eupth2lem3lem3  30300  frcond1  30336  frgr1v  30341  nfrgr2v  30342  frgr3v  30345  1vwmgr  30346  3vfriswmgr  30348  3cyclfrgrrn1  30355  n4cyclfrgr  30361  frgrwopreglem4a  30380  h1de2ctlem  31626  spansn  31630  elspansn  31637  elspansn2  31638  spansneleq  31641  h1datom  31653  spansnj  31718  spansncv  31724  superpos  32425  sumdmdlem2  32490  aciunf1lem  32735  fnpreimac  32743  dfcnv2  32748  pwrssmgc  33060  gsummpt2co  33109  gsumpart  33124  gsumwrd2dccatlem  33138  gsumwrd2dccat  33139  0nellinds  33430  lindssn  33438  lsmsnidl  33459  nsgmgclem  33471  nsgmgc  33472  nsgqusf1olem1  33473  nsgqusf1olem2  33474  nsgqusf1olem3  33475  pidlnzb  33482  elrspunidl  33488  extvfval  33676  esplyfval1  33717  esplyfvaln  33718  lbslsat  33760  lindsunlem  33768  extdgval  33797  fldextrspunlsplem  33817  locfinreflem  33984  esum2dlem  34236  sibfima  34482  sibfof  34484  bnj1373  35172  bnj1489  35198  funen1cnv  35231  fineqvac  35260  cplgredgex  35303  pfxwlk  35306  revwlk  35307  loop1cycl  35319  cvmscbv  35440  cvmsdisj  35452  cvmsss2  35456  cvmliftlem15  35480  cvmlift2lem11  35495  cvmlift2lem12  35496  cvmlift2lem13  35497  satffunlem1lem1  35584  satffunlem2lem1  35586  mvtinf  35737  eldm3  35943  elima4  35958  fvsingle  36100  snelsingles  36102  dfiota3  36103  brapply  36118  funpartlem  36124  altopeq12  36144  ranksng  36349  neibastop3  36544  tailval  36555  filnetlem4  36563  ttcid  36674  mh-inf3sn  36724  mh-infprim2bi  36729  mh-infprim3bi  36730  bj-snexg  37341  bj-restsnss  37395  bj-restsnss2  37396  f1omptsnlem  37652  f1omptsn  37653  mptsnun  37655  dissneqlem  37656  dissneq  37657  fvineqsnf1  37726  lindsadd  37934  lindsenlbs  37936  poimirlem4  37945  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem31  37972  poimirlem32  37973  heiborlem3  38134  ismrer1  38159  lshpnel2N  39431  lsatlspsn2  39438  lsatlspsn  39439  lsatspn0  39446  lkrscss  39544  lfl1dim  39567  lfl1dim2N  39568  ldualvs  39583  atpointN  40189  watvalN  40439  trnsetN  40602  dih1dimatlem  41775  dihatexv  41784  dihjat1lem  41874  dihjat1  41875  lcfl7N  41947  lcfl8  41948  lcfl9a  41951  lcfrlem8  41995  lcfrlem9  41996  lcf1o  41997  mapdval2N  42076  mapdval4N  42078  mapdspex  42114  mapdn0  42115  mapdpglem23  42140  mapdpg  42152  mapdindp1  42166  mapdheq  42174  hvmapval  42206  mapdh9a  42235  hdmap1eq  42247  hdmap1cbv  42248  hdmapval  42274  hdmap10  42286  hdmaplkr  42359  sn-iotalem  42662  evlsevl  43007  0prjspnrel  43060  mzpclval  43157  mzpcl1  43161  wopprc  43458  dnnumch3lem  43474  aomclem8  43489  mendvsca  43615  cytpval  43630  snen1g  43951  k0004lem3  44576  dvconstbi  44761  relpfrlem  45380  permaxinf2lem  45439  wessf1ornlem  45615  dvmptfprodlem  46372  fourierdlem32  46567  fourierdlem33  46568  fourierdlem48  46582  funressnmo  47494  aiotajust  47532  funressndmafv2rn  47671  fzopredsuc  47772  elsprel  47935  clnbgrval  48298  dfvopnbgr2  48329  vopnbgrel  48330  dfclnbgr6  48332  dfnbgr6  48333  cycl3grtri  48423  dmmpossx2  48813  lindslinindsimp2  48939  ldepspr  48949  ldepsnlinc  48984  line  49208  rrxline  49210  dftpos5  49349  tposideq  49363  initc  49566  setc2othin  49941  functermceu  49985  idfudiag1  50000  funcsn  50016  0fucterm  50018  mndtcval  50054  mndtcbas  50056