Theorem sneq 4602

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

Syntax hints:   → wi 4   = wceq 1540  {cab 2708  {csn 4592

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-sn 4593

This theorem is referenced by:  sneqi  4603  sneqd  4604  euabsn  4693  absneu  4695  preq1  4700  tpeq3  4711  issn  4799  mosneq  4809  sneqbg  4810  opeq1  4840  snexg  5393  propeqop  5470  opthwiener  5477  otiunsndisj  5483  opeliunxp  5708  opeliun2xp  5709  relop  5817  inisegn0  6072  xpdifid  6144  dmsnsnsn  6196  predeq123  6278  iotajust  6466  iotanul2  6484  fconstg  6750  f1osng  6844  opabiotafun  6944  fvn0ssdmfun  7049  fsng  7112  fsn2g  7113  fnressn  7133  fressnfv  7135  funfvima3  7213  f12dfv  7251  f13dfv  7252  isofrlem  7318  isoselem  7319  elxp4  7901  elxp5  7902  1stval  7973  2ndval  7974  2ndval2  7989  fo1st  7991  fo2nd  7992  f1stres  7995  f2ndres  7996  mpomptsx  8046  dmmpossx  8048  fmpox  8049  ovmptss  8075  fparlem3  8096  fparlem4  8097  xpord2pred  8127  xpord3pred  8134  suppval  8144  suppsnop  8160  ressuppssdif  8167  brtpos2  8214  dftpos4  8227  tpostpos  8228  naddcllem  8643  eceq1  8713  fvdiagfn  8867  mapsncnv  8869  elixpsn  8913  ixpsnf1o  8914  ensn1g  8996  en1  8998  difsnen  9027  xpsneng  9030  xpcomco  9036  xpassen  9040  xpdom2  9041  canth2  9100  rexdif1en  9128  rexdif1enOLD  9129  cnvfi  9146  xpfiOLD  9277  marypha2lem2  9394  cardsn  9929  pm54.43  9961  dfac5lem3  10085  dfac5lem4  10086  dfac5lem4OLD  10088  kmlem9  10119  kmlem11  10121  kmlem12  10122  ackbij1lem8  10186  r1om  10203  fictb  10204  hsmexlem4  10389  axcc2lem  10396  axcc2  10397  axdc3lem4  10413  fpwwe2cbv  10590  fpwwe2lem3  10593  fpwwecbv  10604  canth4  10607  s3iunsndisj  14941  fsum2dlem  15743  fsumcnv  15746  fsumcom2  15747  ackbijnn  15801  fprod2dlem  15953  fprodcnv  15956  fprodcom2  15957  lcmfunsnlem1  16614  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  lcmfunsnlem2  16617  lcmfunsn  16621  vdwlem1  16959  vdwlem12  16970  vdwlem13  16971  vdwnn  16976  0ram  16998  ramz2  17002  pwsval  17456  symg2bas  19330  symgfixelsi  19372  pmtrfv  19389  pmtrprfval  19424  sylow2a  19556  efgrelexlema  19686  gsum2dlem2  19908  gsum2d2  19911  gsumcom2  19912  dprdcntz  19947  dprddisj  19948  dprd2dlem2  19979  dprd2dlem1  19980  dprd2da  19981  ablfac1eu  20012  ablfaclem3  20026  lssats2  20913  lspsneq0  20925  lbsind  20994  lspsneq  21039  lspdisj2  21044  lspsnsubn0  21057  lspprat  21070  islbs2  21071  lbsextlem4  21078  lbsextg  21079  lpi0  21243  lpi1  21244  irinitoringc  21396  pzriprnglem13  21410  pzriprnglem14  21411  frlmlbs  21713  lindfind  21732  lindsind  21733  lindfrn  21737  psrvsca  21865  evlssca  22003  mpfind  22021  coe1fv  22098  coe1tm  22166  pf1ind  22249  submaval  22475  mdetunilem3  22508  mdetunilem4  22509  mdetunilem9  22514  islp  23034  perfi  23049  t1sncld  23220  bwth  23304  dis2ndc  23354  nllyi  23369  dissnlocfin  23423  ptbasfi  23475  txkgen  23546  xkofvcn  23578  xkoinjcn  23581  qtopeu  23610  txswaphmeolem  23698  pt1hmeo  23700  elflim2  23858  cnextfvval  23959  cnextcn  23961  cnextfres1  23962  cnextfres  23963  tsmsxplem1  24047  tsmsxplem2  24048  ucncn  24179  itg11  25599  i1faddlem  25601  i1fmullem  25602  itg1addlem3  25606  itg1mulc  25612  eldv  25806  ply1lpir  26094  areambl  26875  conway  27718  scutval  27719  scutcut  27720  scutbday  27723  eqscut  27724  eqscut2  27725  scutun12  27729  scutbdaybnd  27734  scutbdaybnd2  27735  scutbdaylt  27737  bday1s  27750  cuteq0  27751  cuteq1  27753  madebdaylemlrcut  27817  cofcut1  27835  cofcutr  27839  onsiso  28176  bdayn0p1  28265  expsval  28318  tglngval  28485  edglnl  29077  nbgrval  29270  nbgr2vtx1edg  29284  nbuhgr2vtx1edgb  29286  nbgr1vtx  29292  nb3grprlem2  29315  uvtxel  29322  uvtxel1  29330  uvtxusgrel  29337  cusgredg  29358  cplgr1v  29364  cplgr3v  29369  usgredgsscusgredg  29394  vtxdgval  29403  1loopgrvd2  29438  wlk1walk  29574  wlkres  29605  wlkp1lem8  29615  usgr2pthlem  29700  crctcshwlkn0lem6  29752  2wspiundisj  29900  clwwlknon1  30033  1wlkdlem4  30076  eupth2lem3lem3  30166  frcond1  30202  frgr1v  30207  nfrgr2v  30208  frgr3v  30211  1vwmgr  30212  3vfriswmgr  30214  3cyclfrgrrn1  30221  n4cyclfrgr  30227  frgrwopreglem4a  30246  h1de2ctlem  31491  spansn  31495  elspansn  31502  elspansn2  31503  spansneleq  31506  h1datom  31518  spansnj  31583  spansncv  31589  superpos  32290  sumdmdlem2  32355  aciunf1lem  32593  fnpreimac  32602  dfcnv2  32607  pwrssmgc  32933  gsummpt2co  32995  gsumpart  33004  gsumwrd2dccatlem  33013  gsumwrd2dccat  33014  0nellinds  33348  lindssn  33356  lsmsnidl  33377  nsgmgclem  33389  nsgmgc  33390  nsgqusf1olem1  33391  nsgqusf1olem2  33392  nsgqusf1olem3  33393  pidlnzb  33400  elrspunidl  33406  lbslsat  33619  lindsunlem  33627  extdgval  33656  fldextrspunlsplem  33675  locfinreflem  33837  esum2dlem  34089  sibfima  34336  sibfof  34338  bnj1373  35027  bnj1489  35053  funen1cnv  35085  fineqvac  35094  cplgredgex  35115  pfxwlk  35118  revwlk  35119  loop1cycl  35131  cvmscbv  35252  cvmsdisj  35264  cvmsss2  35268  cvmliftlem15  35292  cvmlift2lem11  35307  cvmlift2lem12  35308  cvmlift2lem13  35309  satffunlem1lem1  35396  satffunlem2lem1  35398  mvtinf  35549  eldm3  35755  elima4  35770  fvsingle  35915  snelsingles  35917  dfiota3  35918  brapply  35933  funpartlem  35937  altopeq12  35957  ranksng  36162  neibastop3  36357  tailval  36368  filnetlem4  36376  bj-snexg  37029  bj-restsnss  37078  bj-restsnss2  37079  f1omptsnlem  37331  f1omptsn  37332  mptsnun  37334  dissneqlem  37335  dissneq  37336  fvineqsnf1  37405  lindsadd  37614  lindsenlbs  37616  poimirlem4  37625  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem31  37652  poimirlem32  37653  heiborlem3  37814  ismrer1  37839  lshpnel2N  38985  lsatlspsn2  38992  lsatlspsn  38993  lsatspn0  39000  lkrscss  39098  lfl1dim  39121  lfl1dim2N  39122  ldualvs  39137  atpointN  39744  watvalN  39994  trnsetN  40157  dih1dimatlem  41330  dihatexv  41339  dihjat1lem  41429  dihjat1  41430  lcfl7N  41502  lcfl8  41503  lcfl9a  41506  lcfrlem8  41550  lcfrlem9  41551  lcf1o  41552  mapdval2N  41631  mapdval4N  41633  mapdspex  41669  mapdn0  41670  mapdpglem23  41695  mapdpg  41707  mapdindp1  41721  mapdheq  41729  hvmapval  41761  mapdh9a  41790  hdmap1eq  41802  hdmap1cbv  41803  hdmapval  41829  hdmap10  41841  hdmaplkr  41914  sn-iotalem  42216  evlsvvval  42558  evlsevl  42566  0prjspnrel  42622  mzpclval  42720  mzpcl1  42724  wopprc  43026  dnnumch3lem  43042  aomclem8  43057  mendvsca  43183  cytpval  43198  snen1g  43520  k0004lem3  44145  dvconstbi  44330  relpfrlem  44950  permaxinf2lem  45009  wessf1ornlem  45186  dvmptfprodlem  45949  fourierdlem32  46144  fourierdlem33  46145  fourierdlem48  46159  funressnmo  47051  aiotajust  47089  funressndmafv2rn  47228  fzopredsuc  47328  elsprel  47480  clnbgrval  47827  dfvopnbgr2  47857  vopnbgrel  47858  dfclnbgr6  47860  dfnbgr6  47861  cycl3grtri  47950  dmmpossx2  48329  lindslinindsimp2  48456  ldepspr  48466  ldepsnlinc  48501  line  48725  rrxline  48727  dftpos5  48866  tposideq  48880  initc  49084  setc2othin  49459  functermceu  49503  idfudiag1  49518  funcsn  49534  0fucterm  49536  mndtcval  49572  mndtcbas  49574