Theorem sneq 4595

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 2741	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2795	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4586	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4586	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1540  {cab 2707  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-sn 4586

This theorem is referenced by:  sneqi  4596  sneqd  4597  euabsn  4686  absneu  4688  preq1  4693  tpeq3  4704  issn  4792  mosneq  4802  sneqbg  4803  opeq1  4833  snexg  5385  propeqop  5462  opthwiener  5469  otiunsndisj  5475  opeliunxp  5698  opeliun2xp  5699  relop  5804  inisegn0  6058  xpdifid  6129  dmsnsnsn  6181  predeq123  6263  iotajust  6451  iotanul2  6469  fconstg  6729  f1osng  6823  opabiotafun  6923  fvn0ssdmfun  7028  fsng  7091  fsn2g  7092  fnressn  7112  fressnfv  7114  funfvima3  7192  f12dfv  7230  f13dfv  7231  isofrlem  7297  isoselem  7298  elxp4  7878  elxp5  7879  1stval  7949  2ndval  7950  2ndval2  7965  fo1st  7967  fo2nd  7968  f1stres  7971  f2ndres  7972  mpomptsx  8022  dmmpossx  8024  fmpox  8025  ovmptss  8049  fparlem3  8070  fparlem4  8071  xpord2pred  8101  xpord3pred  8108  suppval  8118  suppsnop  8134  ressuppssdif  8141  brtpos2  8188  dftpos4  8201  tpostpos  8202  naddcllem  8617  eceq1  8687  fvdiagfn  8841  mapsncnv  8843  elixpsn  8887  ixpsnf1o  8888  ensn1g  8970  en1  8972  difsnen  9000  xpsneng  9003  xpcomco  9008  xpassen  9012  xpdom2  9013  canth2  9071  rexdif1en  9099  rexdif1enOLD  9100  cnvfi  9117  xpfiOLD  9246  marypha2lem2  9363  cardsn  9898  pm54.43  9930  dfac5lem3  10054  dfac5lem4  10055  dfac5lem4OLD  10057  kmlem9  10088  kmlem11  10090  kmlem12  10091  ackbij1lem8  10155  r1om  10172  fictb  10173  hsmexlem4  10358  axcc2lem  10365  axcc2  10366  axdc3lem4  10382  fpwwe2cbv  10559  fpwwe2lem3  10562  fpwwecbv  10573  canth4  10576  s3iunsndisj  14910  fsum2dlem  15712  fsumcnv  15715  fsumcom2  15716  ackbijnn  15770  fprod2dlem  15922  fprodcnv  15925  fprodcom2  15926  lcmfunsnlem1  16583  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  lcmfunsnlem2  16586  lcmfunsn  16590  vdwlem1  16928  vdwlem12  16939  vdwlem13  16940  vdwnn  16945  0ram  16967  ramz2  16971  pwsval  17425  symg2bas  19299  symgfixelsi  19341  pmtrfv  19358  pmtrprfval  19393  sylow2a  19525  efgrelexlema  19655  gsum2dlem2  19877  gsum2d2  19880  gsumcom2  19881  dprdcntz  19916  dprddisj  19917  dprd2dlem2  19948  dprd2dlem1  19949  dprd2da  19950  ablfac1eu  19981  ablfaclem3  19995  lssats2  20882  lspsneq0  20894  lbsind  20963  lspsneq  21008  lspdisj2  21013  lspsnsubn0  21026  lspprat  21039  islbs2  21040  lbsextlem4  21047  lbsextg  21048  lpi0  21212  lpi1  21213  irinitoringc  21365  pzriprnglem13  21379  pzriprnglem14  21380  frlmlbs  21682  lindfind  21701  lindsind  21702  lindfrn  21706  psrvsca  21834  evlssca  21972  mpfind  21990  coe1fv  22067  coe1tm  22135  pf1ind  22218  submaval  22444  mdetunilem3  22477  mdetunilem4  22478  mdetunilem9  22483  islp  23003  perfi  23018  t1sncld  23189  bwth  23273  dis2ndc  23323  nllyi  23338  dissnlocfin  23392  ptbasfi  23444  txkgen  23515  xkofvcn  23547  xkoinjcn  23550  qtopeu  23579  txswaphmeolem  23667  pt1hmeo  23669  elflim2  23827  cnextfvval  23928  cnextcn  23930  cnextfres1  23931  cnextfres  23932  tsmsxplem1  24016  tsmsxplem2  24017  ucncn  24148  itg11  25568  i1faddlem  25570  i1fmullem  25571  itg1addlem3  25575  itg1mulc  25581  eldv  25775  ply1lpir  26063  areambl  26844  conway  27687  scutval  27688  scutcut  27689  scutbday  27692  eqscut  27693  eqscut2  27694  scutun12  27698  scutbdaybnd  27703  scutbdaybnd2  27704  scutbdaylt  27706  bday1s  27719  cuteq0  27720  cuteq1  27722  madebdaylemlrcut  27786  cofcut1  27804  cofcutr  27808  onsiso  28145  bdayn0p1  28234  expsval  28287  tglngval  28454  edglnl  29046  nbgrval  29239  nbgr2vtx1edg  29253  nbuhgr2vtx1edgb  29255  nbgr1vtx  29261  nb3grprlem2  29284  uvtxel  29291  uvtxel1  29299  uvtxusgrel  29306  cusgredg  29327  cplgr1v  29333  cplgr3v  29338  usgredgsscusgredg  29363  vtxdgval  29372  1loopgrvd2  29407  wlk1walk  29542  wlkres  29572  wlkp1lem8  29582  usgr2pthlem  29666  crctcshwlkn0lem6  29718  2wspiundisj  29866  clwwlknon1  29999  1wlkdlem4  30042  eupth2lem3lem3  30132  frcond1  30168  frgr1v  30173  nfrgr2v  30174  frgr3v  30177  1vwmgr  30178  3vfriswmgr  30180  3cyclfrgrrn1  30187  n4cyclfrgr  30193  frgrwopreglem4a  30212  h1de2ctlem  31457  spansn  31461  elspansn  31468  elspansn2  31469  spansneleq  31472  h1datom  31484  spansnj  31549  spansncv  31555  superpos  32256  sumdmdlem2  32321  aciunf1lem  32559  fnpreimac  32568  dfcnv2  32573  pwrssmgc  32899  gsummpt2co  32961  gsumpart  32970  gsumwrd2dccatlem  32979  gsumwrd2dccat  32980  0nellinds  33314  lindssn  33322  lsmsnidl  33343  nsgmgclem  33355  nsgmgc  33356  nsgqusf1olem1  33357  nsgqusf1olem2  33358  nsgqusf1olem3  33359  pidlnzb  33366  elrspunidl  33372  lbslsat  33585  lindsunlem  33593  extdgval  33622  fldextrspunlsplem  33641  locfinreflem  33803  esum2dlem  34055  sibfima  34302  sibfof  34304  bnj1373  34993  bnj1489  35019  funen1cnv  35051  fineqvac  35060  cplgredgex  35081  pfxwlk  35084  revwlk  35085  loop1cycl  35097  cvmscbv  35218  cvmsdisj  35230  cvmsss2  35234  cvmliftlem15  35258  cvmlift2lem11  35273  cvmlift2lem12  35274  cvmlift2lem13  35275  satffunlem1lem1  35362  satffunlem2lem1  35364  mvtinf  35515  eldm3  35721  elima4  35736  fvsingle  35881  snelsingles  35883  dfiota3  35884  brapply  35899  funpartlem  35903  altopeq12  35923  ranksng  36128  neibastop3  36323  tailval  36334  filnetlem4  36342  bj-snexg  36995  bj-restsnss  37044  bj-restsnss2  37045  f1omptsnlem  37297  f1omptsn  37298  mptsnun  37300  dissneqlem  37301  dissneq  37302  fvineqsnf1  37371  lindsadd  37580  lindsenlbs  37582  poimirlem4  37591  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  poimirlem31  37618  poimirlem32  37619  heiborlem3  37780  ismrer1  37805  lshpnel2N  38951  lsatlspsn2  38958  lsatlspsn  38959  lsatspn0  38966  lkrscss  39064  lfl1dim  39087  lfl1dim2N  39088  ldualvs  39103  atpointN  39710  watvalN  39960  trnsetN  40123  dih1dimatlem  41296  dihatexv  41305  dihjat1lem  41395  dihjat1  41396  lcfl7N  41468  lcfl8  41469  lcfl9a  41472  lcfrlem8  41516  lcfrlem9  41517  lcf1o  41518  mapdval2N  41597  mapdval4N  41599  mapdspex  41635  mapdn0  41636  mapdpglem23  41661  mapdpg  41673  mapdindp1  41687  mapdheq  41695  hvmapval  41727  mapdh9a  41756  hdmap1eq  41768  hdmap1cbv  41769  hdmapval  41795  hdmap10  41807  hdmaplkr  41880  sn-iotalem  42182  evlsvvval  42524  evlsevl  42532  0prjspnrel  42588  mzpclval  42686  mzpcl1  42690  wopprc  42992  dnnumch3lem  43008  aomclem8  43023  mendvsca  43149  cytpval  43164  snen1g  43486  k0004lem3  44111  dvconstbi  44296  relpfrlem  44916  permaxinf2lem  44975  wessf1ornlem  45152  dvmptfprodlem  45915  fourierdlem32  46110  fourierdlem33  46111  fourierdlem48  46125  funressnmo  47020  aiotajust  47058  funressndmafv2rn  47197  fzopredsuc  47297  elsprel  47449  clnbgrval  47796  dfvopnbgr2  47826  vopnbgrel  47827  dfclnbgr6  47829  dfnbgr6  47830  cycl3grtri  47919  dmmpossx2  48298  lindslinindsimp2  48425  ldepspr  48435  ldepsnlinc  48470  line  48694  rrxline  48696  dftpos5  48835  tposideq  48849  initc  49053  setc2othin  49428  functermceu  49472  idfudiag1  49487  funcsn  49503  0fucterm  49505  mndtcval  49541  mndtcbas  49543