Theorem sneq 4636

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

Syntax hints:   → wi 4   = wceq 1540  {cab 2714  {csn 4626

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-sn 4627

This theorem is referenced by:  sneqi  4637  sneqd  4638  euabsn  4726  absneu  4728  preq1  4733  tpeq3  4744  issn  4832  mosneq  4842  sneqbg  4843  opeq1  4873  snexg  5435  propeqop  5512  opthwiener  5519  otiunsndisj  5525  opeliunxp  5752  opeliun2xp  5753  relop  5861  inisegn0  6116  xpdifid  6188  dmsnsnsn  6240  predeq123  6322  suceq  6450  iotajust  6513  iotanul2  6531  fconstg  6795  f1osng  6889  opabiotafun  6989  fvn0ssdmfun  7094  fsng  7157  fsn2g  7158  fnressn  7178  fressnfv  7180  funfvima3  7256  f12dfv  7293  f13dfv  7294  isofrlem  7360  isoselem  7361  elxp4  7944  elxp5  7945  1stval  8016  2ndval  8017  2ndval2  8032  fo1st  8034  fo2nd  8035  f1stres  8038  f2ndres  8039  mpomptsx  8089  dmmpossx  8091  fmpox  8092  ovmptss  8118  fparlem3  8139  fparlem4  8140  xpord2pred  8170  xpord3pred  8177  suppval  8187  suppsnop  8203  ressuppssdif  8210  brtpos2  8257  dftpos4  8270  tpostpos  8271  naddcllem  8714  eceq1  8784  fvdiagfn  8931  mapsncnv  8933  elixpsn  8977  ixpsnf1o  8978  ensn1g  9062  en1  9064  difsnen  9093  xpsneng  9096  xpcomco  9102  xpassen  9106  xpdom2  9107  canth2  9170  rexdif1en  9198  rexdif1enOLD  9199  cnvfi  9216  phplem3OLD  9256  xpfiOLD  9359  marypha2lem2  9476  cardsn  10009  pm54.43  10041  dfac5lem3  10165  dfac5lem4  10166  dfac5lem4OLD  10168  kmlem9  10199  kmlem11  10201  kmlem12  10202  ackbij1lem8  10266  r1om  10283  fictb  10284  hsmexlem4  10469  axcc2lem  10476  axcc2  10477  axdc3lem4  10493  fpwwe2cbv  10670  fpwwe2lem3  10673  fpwwecbv  10684  canth4  10687  s3iunsndisj  15007  fsum2dlem  15806  fsumcnv  15809  fsumcom2  15810  ackbijnn  15864  fprod2dlem  16016  fprodcnv  16019  fprodcom2  16020  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  lcmfunsn  16681  vdwlem1  17019  vdwlem12  17030  vdwlem13  17031  vdwnn  17036  0ram  17058  ramz2  17062  pwsval  17531  symg2bas  19410  symgfixelsi  19453  pmtrfv  19470  pmtrprfval  19505  sylow2a  19637  efgrelexlema  19767  gsum2dlem2  19989  gsum2d2  19992  gsumcom2  19993  dprdcntz  20028  dprddisj  20029  dprd2dlem2  20060  dprd2dlem1  20061  dprd2da  20062  ablfac1eu  20093  ablfaclem3  20107  lssats2  20998  lspsneq0  21010  lbsind  21079  lspsneq  21124  lspdisj2  21129  lspsnsubn0  21142  lspprat  21155  islbs2  21156  lbsextlem4  21163  lbsextg  21164  lpi0  21336  lpi1  21337  irinitoringc  21490  pzriprnglem13  21504  pzriprnglem14  21505  frlmlbs  21817  lindfind  21836  lindsind  21837  lindfrn  21841  psrvsca  21969  evlssca  22113  mpfind  22131  coe1fv  22208  coe1tm  22276  pf1ind  22359  submaval  22587  mdetunilem3  22620  mdetunilem4  22621  mdetunilem9  22626  islp  23148  perfi  23163  t1sncld  23334  bwth  23418  dis2ndc  23468  nllyi  23483  dissnlocfin  23537  ptbasfi  23589  txkgen  23660  xkofvcn  23692  xkoinjcn  23695  qtopeu  23724  txswaphmeolem  23812  pt1hmeo  23814  elflim2  23972  cnextfvval  24073  cnextcn  24075  cnextfres1  24076  cnextfres  24077  tsmsxplem1  24161  tsmsxplem2  24162  ucncn  24294  itg11  25726  i1faddlem  25728  i1fmullem  25729  itg1addlem3  25733  itg1mulc  25739  eldv  25933  ply1lpir  26221  areambl  27001  conway  27844  scutval  27845  scutcut  27846  scutbday  27849  eqscut  27850  eqscut2  27851  scutun12  27855  scutbdaybnd  27860  scutbdaybnd2  27861  scutbdaylt  27863  bday1s  27876  cuteq0  27877  cuteq1  27878  madebdaylemlrcut  27937  cofcut1  27954  cofcutr  27958  expsval  28408  tglngval  28559  edglnl  29160  nbgrval  29353  nbgr2vtx1edg  29367  nbuhgr2vtx1edgb  29369  nbgr1vtx  29375  nb3grprlem2  29398  uvtxel  29405  uvtxel1  29413  uvtxusgrel  29420  cusgredg  29441  cplgr1v  29447  cplgr3v  29452  usgredgsscusgredg  29477  vtxdgval  29486  1loopgrvd2  29521  wlk1walk  29657  wlkres  29688  wlkp1lem8  29698  usgr2pthlem  29783  crctcshwlkn0lem6  29835  2wspiundisj  29983  clwwlknon1  30116  1wlkdlem4  30159  eupth2lem3lem3  30249  frcond1  30285  frgr1v  30290  nfrgr2v  30291  frgr3v  30294  1vwmgr  30295  3vfriswmgr  30297  3cyclfrgrrn1  30304  n4cyclfrgr  30310  frgrwopreglem4a  30329  h1de2ctlem  31574  spansn  31578  elspansn  31585  elspansn2  31586  spansneleq  31589  h1datom  31601  spansnj  31666  spansncv  31672  superpos  32373  sumdmdlem2  32438  aciunf1lem  32672  fnpreimac  32681  dfcnv2  32686  pwrssmgc  32990  gsummpt2co  33051  gsumpart  33060  gsumwrd2dccatlem  33069  gsumwrd2dccat  33070  0nellinds  33398  lindssn  33406  lsmsnidl  33427  nsgmgclem  33439  nsgmgc  33440  nsgqusf1olem1  33441  nsgqusf1olem2  33442  nsgqusf1olem3  33443  pidlnzb  33450  elrspunidl  33456  lbslsat  33667  lindsunlem  33675  extdgval  33705  fldextrspunlsplem  33723  locfinreflem  33839  esum2dlem  34093  sibfima  34340  sibfof  34342  bnj1373  35044  bnj1489  35070  funen1cnv  35102  fineqvac  35111  cplgredgex  35126  pfxwlk  35129  revwlk  35130  loop1cycl  35142  cvmscbv  35263  cvmsdisj  35275  cvmsss2  35279  cvmliftlem15  35303  cvmlift2lem11  35318  cvmlift2lem12  35319  cvmlift2lem13  35320  satffunlem1lem1  35407  satffunlem2lem1  35409  mvtinf  35560  eldm3  35761  elima4  35776  fvsingle  35921  snelsingles  35923  dfiota3  35924  brapply  35939  funpartlem  35943  altopeq12  35963  ranksng  36168  neibastop3  36363  tailval  36374  filnetlem4  36382  bj-snexg  37035  bj-restsnss  37084  bj-restsnss2  37085  f1omptsnlem  37337  f1omptsn  37338  mptsnun  37340  dissneqlem  37341  dissneq  37342  fvineqsnf1  37411  lindsadd  37620  lindsenlbs  37622  poimirlem4  37631  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem31  37658  poimirlem32  37659  heiborlem3  37820  ismrer1  37845  lshpnel2N  38986  lsatlspsn2  38993  lsatlspsn  38994  lsatspn0  39001  lkrscss  39099  lfl1dim  39122  lfl1dim2N  39123  ldualvs  39138  atpointN  39745  watvalN  39995  trnsetN  40158  dih1dimatlem  41331  dihatexv  41340  dihjat1lem  41430  dihjat1  41431  lcfl7N  41503  lcfl8  41504  lcfl9a  41507  lcfrlem8  41551  lcfrlem9  41552  lcf1o  41553  mapdval2N  41632  mapdval4N  41634  mapdspex  41670  mapdn0  41671  mapdpglem23  41696  mapdpg  41708  mapdindp1  41722  mapdheq  41730  hvmapval  41762  mapdh9a  41791  hdmap1eq  41803  hdmap1cbv  41804  hdmapval  41830  hdmap10  41842  hdmaplkr  41915  sn-iotalem  42260  evlsvvval  42573  evlsevl  42581  0prjspnrel  42637  mzpclval  42736  mzpcl1  42740  wopprc  43042  dnnumch3lem  43058  aomclem8  43073  mendvsca  43199  cytpval  43214  snen1g  43537  k0004lem3  44162  dvconstbi  44353  relpfrlem  44974  wessf1ornlem  45190  dvmptfprodlem  45959  fourierdlem32  46154  fourierdlem33  46155  fourierdlem48  46169  funressnmo  47058  aiotajust  47096  funressndmafv2rn  47235  fzopredsuc  47335  elsprel  47462  clnbgrval  47809  dfvopnbgr2  47839  vopnbgrel  47840  dfclnbgr6  47842  dfnbgr6  47843  cycl3grtri  47914  dmmpossx2  48253  lindslinindsimp2  48380  ldepspr  48390  ldepsnlinc  48425  line  48653  rrxline  48655  dftpos5  48774  tposideq  48788  setc2othin  49113  functermceu  49142  mndtcval  49176  mndtcbas  49178