Theorem sneq 4594

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 2772	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2826	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4585	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4585	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2820	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {cab 2738  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-sn 4585

This theorem is used by:  sneqi  4595  sneqd  4596  euabsn  4687  absneu  4689  preq1  4694  tpeq3  4705  issn  4792  mosneq  4802  sneqbg  4803  opeq1  4833  snexgALT  5406  propeqop  5484  opthwiener  5491  otiunsndisj  5497  opeliunxp  5722  opeliun2xp  5723  relop  5830  inisegn0  6094  xpdifid  6160  xpdifcnvepel  6161  dmsnsnsn  6216  predeq123  6300  iotajust  6488  iotanul2  6506  fconstg  6762  f1osng  6860  opabiotafun  6958  fvn0ssdmfun  7067  fsng  7131  fsn2g  7132  fnressn  7155  fressnfv  7157  funfvima3  7235  f12dfv  7274  f13dfv  7275  isofrlem  7341  isoselem  7342  elxp4  7919  elxp5  7920  1stval  7988  2ndval  7989  2ndval2  8004  fo1st  8006  fo2nd  8007  f1stres  8010  f2ndres  8011  mpomptsx  8061  dmmpossx  8063  fmpox  8064  ovmptss  8090  fparlem3  8111  fparlem4  8112  xpord2pred  8143  xpord3pred  8150  suppval  8160  suppsnop  8176  ressuppssdif  8183  brtpos2  8230  dftpos4  8243  tpostpos  8244  naddcllem  8664  eceq1  8736  fvdiagfn  8898  mapsncnv  8900  elixpsn  8944  ixpsnf1o  8945  ensn1g  9028  en1  9030  funen1cnv  9035  difsnen  9057  xpsneng  9060  xpcomco  9065  xpassen  9069  xpdom2  9070  canth2  9128  rexdif1en  9155  cnvfi  9170  marypha2lem2  9406  cardsn  9974  pm54.43  10006  dfac5lem3  10128  dfac5lem4  10129  kmlem9  10161  kmlem11  10163  kmlem12  10164  ackbij1lem8  10228  r1om  10245  fictb  10246  hsmexlem4  10431  axcc2lem  10438  axcc2  10439  axdc3lem4  10455  fpwwe2cbv  10639  fpwwe2lem3  10642  fpwwecbv  10653  canth4  10656  s3iunsndisj  15041  fsum2dlem  15856  fsumcnv  15859  fsumcom2  15860  ackbijnn  15917  fprod2dlem  16067  fprodcnv  16070  fprodcom2  16071  lcmfunsnlem1  16727  lcmfunsnlem2lem1  16728  lcmfunsnlem2lem2  16729  lcmfunsnlem2  16730  lcmfunsn  16734  vdwlem1  17073  vdwlem12  17084  vdwlem13  17085  vdwnn  17090  0ram  17112  ramz2  17116  pwsval  17571  symg2bas  19520  symgfixelsi  19562  pmtrfv  19579  pmtrprfval  19614  sylow2a  19746  efgrelexlema  19876  gsum2dlem2  20098  gsum2d2  20101  gsumcom2  20102  dprdcntz  20137  dprddisj  20138  dprd2dlem2  20169  dprd2dlem1  20170  dprd2da  20171  ablfac1eu  20202  ablfaclem3  20216  lssats2  21184  lspsneq0  21196  lbsind  21264  lspsneq  21309  lspdisj2  21314  lspsnsubn0  21327  lspprat  21340  islbs2  21341  lbsextlem4  21348  lbsextg  21349  lpi0  21557  lpi1  21558  irinitoringc  21692  pzriprnglem13  21706  pzriprnglem14  21707  frlmlbs  22010  lindfind  22029  lindsind  22030  lindfrn  22034  lindsenlbs  22064  psrvsca  22164  evlsvvval  22309  evlssca  22310  mpfind  22331  evlsevl  22348  coe1fv  22431  coe1tm  22499  pf1ind  22580  submaval  22803  mdetunilem3  22836  mdetunilem4  22837  mdetunilem9  22842  islp  23365  perfi  23380  t1sncld  23551  bwth  23635  dis2ndc  23686  nllyi  23701  dissnlocfin  23755  ptbasfi  23807  txkgen  23878  xkofvcn  23910  xkoinjcn  23913  qtopeu  23942  txswaphmeolem  24030  pt1hmeo  24032  elflim2  24190  cnextfvval  24291  cnextcn  24293  cnextfres1  24294  cnextfres  24295  tsmsxplem1  24379  tsmsxplem2  24380  ucncn  24510  itg11  25919  i1faddlem  25921  i1fmullem  25922  itg1addlem3  25926  itg1mulc  25932  eldv  26125  ply1lpir  26407  areambl  27195  conway  28044  cutsval  28045  cutcuts  28046  cutbday  28049  eqcuts  28050  eqcuts2  28051  cutsun12  28055  cutbdaybnd  28060  cutbdaybnd2  28061  cutbdaylt  28063  eqcuts3  28069  bday1  28079  cuteq0  28080  cuteq1  28082  madebdaylemlrcut  28164  sltsbday  28182  cofcut1  28185  cofcutr  28189  oniso  28536  bdayn0p1  28634  expsval  28690  pw2cut2  28727  tglngval  28893  edglnl  29600  nbgrval  29796  nbgr2vtx1edg  29810  nbuhgr2vtx1edgb  29812  nbgr1vtx  29818  nb3grprlem2  29841  uvtxel  29848  uvtxel1  29856  uvtxusgrel  29863  cusgredg  29884  cplgr1v  29890  cplgr3v  29895  usgredgsscusgredg  29919  vtxdgval  29928  1loopgrvd2  29963  wlk1walk  30098  wlkres  30128  wlkp1lem8  30138  pfxwlk  30145  revwlk  30146  usgr2pthlem  30228  crctcshwlkn0lem6  30283  2wspiundisj  30434  clwwlknon1  30567  1wlkdlem4  30610  loop1cycl  30623  eupth2lem3lem3  30710  frcond1  30746  frgr1v  30751  nfrgr2v  30752  frgr3v  30755  1vwmgr  30756  3vfriswmgr  30758  3cyclfrgrrn1  30765  n4cyclfrgr  30771  frgrwopreglem4a  30790  h1de2ctlem  32036  spansn  32040  elspansn  32047  elspansn2  32048  spansneleq  32051  h1datom  32063  spansnj  32128  spansncv  32134  superpos  32835  sumdmdlem2  32900  aciunf1lem  33135  fnpreimac  33143  dfcnv2  33148  pwrssmgc  33440  gsummpt2co  33488  gsumpart  33503  gsumwrd2dccatlem  33517  gsumwrd2dccat  33518  0nellinds  33805  lindssn  33811  lsmsnidl  33830  nsgmgclem  33840  nsgmgc  33841  nsgqusf1olem1  33842  nsgqusf1olem2  33843  nsgqusf1olem3  33844  pidlnzb  33850  elrspunidl  33856  extvfval  34042  esplyfval1  34083  esplyfvaln  34084  lbslsat  34126  lindsunlem  34134  extdgval  34163  fldextrspunlsplem  34183  locfinreflem  34350  esum2dlem  34602  sibfima  34849  sibfof  34851  bnj1373  35539  bnj1489  35565  fineqvac  35642  onvfowev  35713  cplgredgex  35719  cvmscbv  35837  cvmsdisj  35849  cvmsss2  35853  cvmliftlem15  35877  cvmlift2lem11  35892  cvmlift2lem12  35893  cvmlift2lem13  35894  satffunlem1lem1  35981  satffunlem2lem1  35983  mvtinf  36134  eldm3  36340  elima4  36355  fvsingle  36497  snelsingles  36499  dfiota3  36500  brapply  36515  funpartlem  36521  altopeq12  36542  ranksng  36747  neibastop3  36981  tailval  36992  filnetlem4  37000  ttcid  37111  mh-inf3sn  37161  mh-infprim2bi  37166  mh-infprim3bi  37167  bj-snexg  37778  bj-restsnss  37833  bj-restsnss2  37834  f1omptsnlem  38090  f1omptsn  38091  mptsnun  38093  dissneqlem  38094  dissneq  38095  fvineqsnf1  38164  lindsadd  38367  poimirlem4  38373  poimirlem25  38394  poimirlem26  38395  poimirlem27  38396  poimirlem31  38400  poimirlem32  38401  heiborlem3  38563  ismrer1  38588  lshpnel2N  39858  lsatlspsn2  39865  lsatlspsn  39866  lsatspn0  39873  lkrscss  39971  lfl1dim  39994  lfl1dim2N  39995  ldualvs  40010  atpointN  40616  watvalN  40866  trnsetN  41029  dih1dimatlem  42202  dihatexv  42211  dihjat1lem  42301  dihjat1  42302  lcfl7N  42374  lcfl8  42375  lcfl9a  42378  lcfrlem8  42422  lcfrlem9  42423  lcf1o  42424  mapdval2N  42503  mapdval4N  42505  mapdspex  42541  mapdn0  42542  mapdpglem23  42567  mapdpg  42579  mapdindp1  42593  mapdheq  42601  hvmapval  42633  mapdh9a  42662  hdmap1eq  42674  hdmap1cbv  42675  hdmapval  42701  hdmap10  42713  hdmaplkr  42786  sn-iotalem  43091  0prjspnrel  43473  mzpclval  43570  mzpcl1  43574  wopprc  43871  dnnumch3lem  43887  aomclem8  43902  mendvsca  44028  cytpval  44043  snen1g  44364  k0004lem3  44989  dvconstbi  45158  relpfrlem  45776  permaxinf2lem  45835  wessf1ornlem  46017  dvmptfprodlem  46772  fourierdlem32  46967  fourierdlem33  46968  fourierdlem48  46982  funressnmo  47934  aiotajust  47972  funressndmafv2rn  48111  fzopredsuc  48212  elsprel  48375  clnbgrval  48738  dfvopnbgr2  48769  vopnbgrel  48770  dfclnbgr6  48772  dfnbgr6  48773  cycl3grtri  48863  dmmpossx2  49267  lindslinindsimp2  49393  ldepspr  49403  ldepsnlinc  49438  line  49662  rrxline  49664  dftpos5  49800  tposideq  49814  initc  50017  setc2othin  50392  functermceu  50436  idfudiag1  50451  funcsn  50467  0fucterm  50469  mndtcval  50505  mndtcbas  50507