Theorem sneq 4581

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 2743	. . 3 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	abbidv 2797	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ 𝑥 = 𝐴} = {𝑥 ∣ 𝑥 = 𝐵})
3		df-sn 4572	. 2 ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
4		df-sn 4572	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
5	2, 3, 4	3eqtr4g 2791	1 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1541  {cab 2709  {csn 4571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-sn 4572

This theorem is referenced by:  sneqi  4582  sneqd  4583  euabsn  4674  absneu  4676  preq1  4681  tpeq3  4692  issn  4779  mosneq  4789  sneqbg  4790  opeq1  4820  snexg  5368  propeqop  5442  opthwiener  5449  otiunsndisj  5455  opeliunxp  5678  opeliun2xp  5679  relop  5785  inisegn0  6042  xpdifid  6110  dmsnsnsn  6162  predeq123  6244  iotajust  6431  iotanul2  6449  fconstg  6705  f1osng  6799  opabiotafun  6897  fvn0ssdmfun  7002  fsng  7065  fsn2g  7066  fnressn  7086  fressnfv  7088  funfvima3  7165  f12dfv  7202  f13dfv  7203  isofrlem  7269  isoselem  7270  elxp4  7847  elxp5  7848  1stval  7918  2ndval  7919  2ndval2  7934  fo1st  7936  fo2nd  7937  f1stres  7940  f2ndres  7941  mpomptsx  7991  dmmpossx  7993  fmpox  7994  ovmptss  8018  fparlem3  8039  fparlem4  8040  xpord2pred  8070  xpord3pred  8077  suppval  8087  suppsnop  8103  ressuppssdif  8110  brtpos2  8157  dftpos4  8170  tpostpos  8171  naddcllem  8586  eceq1  8656  fvdiagfn  8810  mapsncnv  8812  elixpsn  8856  ixpsnf1o  8857  ensn1g  8939  en1  8941  difsnen  8967  xpsneng  8970  xpcomco  8975  xpassen  8979  xpdom2  8980  canth2  9038  rexdif1en  9065  cnvfi  9080  marypha2lem2  9315  cardsn  9857  pm54.43  9889  dfac5lem3  10011  dfac5lem4  10012  dfac5lem4OLD  10014  kmlem9  10045  kmlem11  10047  kmlem12  10048  ackbij1lem8  10112  r1om  10129  fictb  10130  hsmexlem4  10315  axcc2lem  10322  axcc2  10323  axdc3lem4  10339  fpwwe2cbv  10516  fpwwe2lem3  10519  fpwwecbv  10530  canth4  10533  s3iunsndisj  14870  fsum2dlem  15672  fsumcnv  15675  fsumcom2  15676  ackbijnn  15730  fprod2dlem  15882  fprodcnv  15885  fprodcom2  15886  lcmfunsnlem1  16543  lcmfunsnlem2lem1  16544  lcmfunsnlem2lem2  16545  lcmfunsnlem2  16546  lcmfunsn  16550  vdwlem1  16888  vdwlem12  16899  vdwlem13  16900  vdwnn  16905  0ram  16927  ramz2  16931  pwsval  17385  symg2bas  19300  symgfixelsi  19342  pmtrfv  19359  pmtrprfval  19394  sylow2a  19526  efgrelexlema  19656  gsum2dlem2  19878  gsum2d2  19881  gsumcom2  19882  dprdcntz  19917  dprddisj  19918  dprd2dlem2  19949  dprd2dlem1  19950  dprd2da  19951  ablfac1eu  19982  ablfaclem3  19996  lssats2  20928  lspsneq0  20940  lbsind  21009  lspsneq  21054  lspdisj2  21059  lspsnsubn0  21072  lspprat  21085  islbs2  21086  lbsextlem4  21093  lbsextg  21094  lpi0  21258  lpi1  21259  irinitoringc  21411  pzriprnglem13  21425  pzriprnglem14  21426  frlmlbs  21729  lindfind  21748  lindsind  21749  lindfrn  21753  psrvsca  21881  evlssca  22019  mpfind  22037  coe1fv  22114  coe1tm  22182  pf1ind  22265  submaval  22491  mdetunilem3  22524  mdetunilem4  22525  mdetunilem9  22530  islp  23050  perfi  23065  t1sncld  23236  bwth  23320  dis2ndc  23370  nllyi  23385  dissnlocfin  23439  ptbasfi  23491  txkgen  23562  xkofvcn  23594  xkoinjcn  23597  qtopeu  23626  txswaphmeolem  23714  pt1hmeo  23716  elflim2  23874  cnextfvval  23975  cnextcn  23977  cnextfres1  23978  cnextfres  23979  tsmsxplem1  24063  tsmsxplem2  24064  ucncn  24194  itg11  25614  i1faddlem  25616  i1fmullem  25617  itg1addlem3  25621  itg1mulc  25627  eldv  25821  ply1lpir  26109  areambl  26890  conway  27735  scutval  27736  scutcut  27737  scutbday  27740  eqscut  27741  eqscut2  27742  scutun12  27746  scutbdaybnd  27751  scutbdaybnd2  27752  scutbdaylt  27754  eqscut3  27760  bday1s  27770  cuteq0  27771  cuteq1  27773  madebdaylemlrcut  27839  cofcut1  27859  cofcutr  27863  onsiso  28200  bdayn0p1  28289  expsval  28343  pw2cut2  28377  tglngval  28524  edglnl  29116  nbgrval  29309  nbgr2vtx1edg  29323  nbuhgr2vtx1edgb  29325  nbgr1vtx  29331  nb3grprlem2  29354  uvtxel  29361  uvtxel1  29369  uvtxusgrel  29376  cusgredg  29397  cplgr1v  29403  cplgr3v  29408  usgredgsscusgredg  29433  vtxdgval  29442  1loopgrvd2  29477  wlk1walk  29612  wlkres  29642  wlkp1lem8  29652  usgr2pthlem  29736  crctcshwlkn0lem6  29788  2wspiundisj  29936  clwwlknon1  30069  1wlkdlem4  30112  eupth2lem3lem3  30202  frcond1  30238  frgr1v  30243  nfrgr2v  30244  frgr3v  30247  1vwmgr  30248  3vfriswmgr  30250  3cyclfrgrrn1  30257  n4cyclfrgr  30263  frgrwopreglem4a  30282  h1de2ctlem  31527  spansn  31531  elspansn  31538  elspansn2  31539  spansneleq  31542  h1datom  31554  spansnj  31619  spansncv  31625  superpos  32326  sumdmdlem2  32391  aciunf1lem  32636  fnpreimac  32645  dfcnv2  32650  pwrssmgc  32973  gsummpt2co  33020  gsumpart  33029  gsumwrd2dccatlem  33038  gsumwrd2dccat  33039  0nellinds  33327  lindssn  33335  lsmsnidl  33356  nsgmgclem  33368  nsgmgc  33369  nsgqusf1olem1  33370  nsgqusf1olem2  33371  nsgqusf1olem3  33372  pidlnzb  33379  elrspunidl  33385  lbslsat  33621  lindsunlem  33629  extdgval  33658  fldextrspunlsplem  33678  locfinreflem  33845  esum2dlem  34097  sibfima  34343  sibfof  34345  bnj1373  35034  bnj1489  35060  funen1cnv  35092  fineqvac  35131  cplgredgex  35157  pfxwlk  35160  revwlk  35161  loop1cycl  35173  cvmscbv  35294  cvmsdisj  35306  cvmsss2  35310  cvmliftlem15  35334  cvmlift2lem11  35349  cvmlift2lem12  35350  cvmlift2lem13  35351  satffunlem1lem1  35438  satffunlem2lem1  35440  mvtinf  35591  eldm3  35797  elima4  35812  fvsingle  35954  snelsingles  35956  dfiota3  35957  brapply  35972  funpartlem  35976  altopeq12  35996  ranksng  36201  neibastop3  36396  tailval  36407  filnetlem4  36415  bj-snexg  37068  bj-restsnss  37117  bj-restsnss2  37118  f1omptsnlem  37370  f1omptsn  37371  mptsnun  37373  dissneqlem  37374  dissneq  37375  fvineqsnf1  37444  lindsadd  37653  lindsenlbs  37655  poimirlem4  37664  poimirlem25  37685  poimirlem26  37686  poimirlem27  37687  poimirlem31  37691  poimirlem32  37692  heiborlem3  37853  ismrer1  37878  lshpnel2N  39024  lsatlspsn2  39031  lsatlspsn  39032  lsatspn0  39039  lkrscss  39137  lfl1dim  39160  lfl1dim2N  39161  ldualvs  39176  atpointN  39782  watvalN  40032  trnsetN  40195  dih1dimatlem  41368  dihatexv  41377  dihjat1lem  41467  dihjat1  41468  lcfl7N  41540  lcfl8  41541  lcfl9a  41544  lcfrlem8  41588  lcfrlem9  41589  lcf1o  41590  mapdval2N  41669  mapdval4N  41671  mapdspex  41707  mapdn0  41708  mapdpglem23  41733  mapdpg  41745  mapdindp1  41759  mapdheq  41767  hvmapval  41799  mapdh9a  41828  hdmap1eq  41840  hdmap1cbv  41841  hdmapval  41867  hdmap10  41879  hdmaplkr  41952  sn-iotalem  42254  evlsvvval  42596  evlsevl  42604  0prjspnrel  42660  mzpclval  42758  mzpcl1  42762  wopprc  43063  dnnumch3lem  43079  aomclem8  43094  mendvsca  43220  cytpval  43235  snen1g  43557  k0004lem3  44182  dvconstbi  44367  relpfrlem  44986  permaxinf2lem  45045  wessf1ornlem  45222  dvmptfprodlem  45982  fourierdlem32  46177  fourierdlem33  46178  fourierdlem48  46192  funressnmo  47077  aiotajust  47115  funressndmafv2rn  47254  fzopredsuc  47354  elsprel  47506  clnbgrval  47853  dfvopnbgr2  47884  vopnbgrel  47885  dfclnbgr6  47887  dfnbgr6  47888  cycl3grtri  47978  dmmpossx2  48368  lindslinindsimp2  48495  ldepspr  48505  ldepsnlinc  48540  line  48764  rrxline  48766  dftpos5  48905  tposideq  48919  initc  49123  setc2othin  49498  functermceu  49542  idfudiag1  49557  funcsn  49573  0fucterm  49575  mndtcval  49611  mndtcbas  49613