Theorem sneq 4611

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

Syntax hints:   → wi 4   = wceq 1540  {cab 2713  {csn 4601

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-sn 4602

This theorem is referenced by:  sneqi  4612  sneqd  4613  euabsn  4702  absneu  4704  preq1  4709  tpeq3  4720  issn  4808  mosneq  4818  sneqbg  4819  opeq1  4849  snexg  5405  propeqop  5482  opthwiener  5489  otiunsndisj  5495  opeliunxp  5721  opeliun2xp  5722  relop  5830  inisegn0  6085  xpdifid  6157  dmsnsnsn  6209  predeq123  6291  suceq  6419  iotajust  6482  iotanul2  6500  fconstg  6764  f1osng  6858  opabiotafun  6958  fvn0ssdmfun  7063  fsng  7126  fsn2g  7127  fnressn  7147  fressnfv  7149  funfvima3  7227  f12dfv  7265  f13dfv  7266  isofrlem  7332  isoselem  7333  elxp4  7916  elxp5  7917  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  8142  xpord3pred  8149  suppval  8159  suppsnop  8175  ressuppssdif  8182  brtpos2  8229  dftpos4  8242  tpostpos  8243  naddcllem  8686  eceq1  8756  fvdiagfn  8903  mapsncnv  8905  elixpsn  8949  ixpsnf1o  8950  ensn1g  9034  en1  9036  difsnen  9065  xpsneng  9068  xpcomco  9074  xpassen  9078  xpdom2  9079  canth2  9142  rexdif1en  9170  rexdif1enOLD  9171  cnvfi  9188  phplem3OLD  9228  xpfiOLD  9329  marypha2lem2  9446  cardsn  9981  pm54.43  10013  dfac5lem3  10137  dfac5lem4  10138  dfac5lem4OLD  10140  kmlem9  10171  kmlem11  10173  kmlem12  10174  ackbij1lem8  10238  r1om  10255  fictb  10256  hsmexlem4  10441  axcc2lem  10448  axcc2  10449  axdc3lem4  10465  fpwwe2cbv  10642  fpwwe2lem3  10645  fpwwecbv  10656  canth4  10659  s3iunsndisj  14985  fsum2dlem  15784  fsumcnv  15787  fsumcom2  15788  ackbijnn  15842  fprod2dlem  15994  fprodcnv  15997  fprodcom2  15998  lcmfunsnlem1  16654  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  lcmfunsnlem2  16657  lcmfunsn  16661  vdwlem1  16999  vdwlem12  17010  vdwlem13  17011  vdwnn  17016  0ram  17038  ramz2  17042  pwsval  17498  symg2bas  19372  symgfixelsi  19414  pmtrfv  19431  pmtrprfval  19466  sylow2a  19598  efgrelexlema  19728  gsum2dlem2  19950  gsum2d2  19953  gsumcom2  19954  dprdcntz  19989  dprddisj  19990  dprd2dlem2  20021  dprd2dlem1  20022  dprd2da  20023  ablfac1eu  20054  ablfaclem3  20068  lssats2  20955  lspsneq0  20967  lbsind  21036  lspsneq  21081  lspdisj2  21086  lspsnsubn0  21099  lspprat  21112  islbs2  21113  lbsextlem4  21120  lbsextg  21121  lpi0  21285  lpi1  21286  irinitoringc  21438  pzriprnglem13  21452  pzriprnglem14  21453  frlmlbs  21755  lindfind  21774  lindsind  21775  lindfrn  21779  psrvsca  21907  evlssca  22045  mpfind  22063  coe1fv  22140  coe1tm  22208  pf1ind  22291  submaval  22517  mdetunilem3  22550  mdetunilem4  22551  mdetunilem9  22556  islp  23076  perfi  23091  t1sncld  23262  bwth  23346  dis2ndc  23396  nllyi  23411  dissnlocfin  23465  ptbasfi  23517  txkgen  23588  xkofvcn  23620  xkoinjcn  23623  qtopeu  23652  txswaphmeolem  23740  pt1hmeo  23742  elflim2  23900  cnextfvval  24001  cnextcn  24003  cnextfres1  24004  cnextfres  24005  tsmsxplem1  24089  tsmsxplem2  24090  ucncn  24221  itg11  25642  i1faddlem  25644  i1fmullem  25645  itg1addlem3  25649  itg1mulc  25655  eldv  25849  ply1lpir  26137  areambl  26918  conway  27761  scutval  27762  scutcut  27763  scutbday  27766  eqscut  27767  eqscut2  27768  scutun12  27772  scutbdaybnd  27777  scutbdaybnd2  27778  scutbdaylt  27780  bday1s  27793  cuteq0  27794  cuteq1  27795  madebdaylemlrcut  27854  cofcut1  27871  cofcutr  27875  expsval  28325  tglngval  28476  edglnl  29068  nbgrval  29261  nbgr2vtx1edg  29275  nbuhgr2vtx1edgb  29277  nbgr1vtx  29283  nb3grprlem2  29306  uvtxel  29313  uvtxel1  29321  uvtxusgrel  29328  cusgredg  29349  cplgr1v  29355  cplgr3v  29360  usgredgsscusgredg  29385  vtxdgval  29394  1loopgrvd2  29429  wlk1walk  29565  wlkres  29596  wlkp1lem8  29606  usgr2pthlem  29691  crctcshwlkn0lem6  29743  2wspiundisj  29891  clwwlknon1  30024  1wlkdlem4  30067  eupth2lem3lem3  30157  frcond1  30193  frgr1v  30198  nfrgr2v  30199  frgr3v  30202  1vwmgr  30203  3vfriswmgr  30205  3cyclfrgrrn1  30212  n4cyclfrgr  30218  frgrwopreglem4a  30237  h1de2ctlem  31482  spansn  31486  elspansn  31493  elspansn2  31494  spansneleq  31497  h1datom  31509  spansnj  31574  spansncv  31580  superpos  32281  sumdmdlem2  32346  aciunf1lem  32586  fnpreimac  32595  dfcnv2  32600  pwrssmgc  32926  gsummpt2co  32988  gsumpart  32997  gsumwrd2dccatlem  33006  gsumwrd2dccat  33007  0nellinds  33331  lindssn  33339  lsmsnidl  33360  nsgmgclem  33372  nsgmgc  33373  nsgqusf1olem1  33374  nsgqusf1olem2  33375  nsgqusf1olem3  33376  pidlnzb  33383  elrspunidl  33389  lbslsat  33602  lindsunlem  33610  extdgval  33641  fldextrspunlsplem  33660  locfinreflem  33817  esum2dlem  34069  sibfima  34316  sibfof  34318  bnj1373  35007  bnj1489  35033  funen1cnv  35065  fineqvac  35074  cplgredgex  35089  pfxwlk  35092  revwlk  35093  loop1cycl  35105  cvmscbv  35226  cvmsdisj  35238  cvmsss2  35242  cvmliftlem15  35266  cvmlift2lem11  35281  cvmlift2lem12  35282  cvmlift2lem13  35283  satffunlem1lem1  35370  satffunlem2lem1  35372  mvtinf  35523  eldm3  35724  elima4  35739  fvsingle  35884  snelsingles  35886  dfiota3  35887  brapply  35902  funpartlem  35906  altopeq12  35926  ranksng  36131  neibastop3  36326  tailval  36337  filnetlem4  36345  bj-snexg  36998  bj-restsnss  37047  bj-restsnss2  37048  f1omptsnlem  37300  f1omptsn  37301  mptsnun  37303  dissneqlem  37304  dissneq  37305  fvineqsnf1  37374  lindsadd  37583  lindsenlbs  37585  poimirlem4  37594  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem31  37621  poimirlem32  37622  heiborlem3  37783  ismrer1  37808  lshpnel2N  38949  lsatlspsn2  38956  lsatlspsn  38957  lsatspn0  38964  lkrscss  39062  lfl1dim  39085  lfl1dim2N  39086  ldualvs  39101  atpointN  39708  watvalN  39958  trnsetN  40121  dih1dimatlem  41294  dihatexv  41303  dihjat1lem  41393  dihjat1  41394  lcfl7N  41466  lcfl8  41467  lcfl9a  41470  lcfrlem8  41514  lcfrlem9  41515  lcf1o  41516  mapdval2N  41595  mapdval4N  41597  mapdspex  41633  mapdn0  41634  mapdpglem23  41659  mapdpg  41671  mapdindp1  41685  mapdheq  41693  hvmapval  41725  mapdh9a  41754  hdmap1eq  41766  hdmap1cbv  41767  hdmapval  41793  hdmap10  41805  hdmaplkr  41878  sn-iotalem  42218  evlsvvval  42533  evlsevl  42541  0prjspnrel  42597  mzpclval  42695  mzpcl1  42699  wopprc  43001  dnnumch3lem  43017  aomclem8  43032  mendvsca  43158  cytpval  43173  snen1g  43495  k0004lem3  44120  dvconstbi  44306  relpfrlem  44926  permaxinf2lem  44985  wessf1ornlem  45157  dvmptfprodlem  45921  fourierdlem32  46116  fourierdlem33  46117  fourierdlem48  46131  funressnmo  47023  aiotajust  47061  funressndmafv2rn  47200  fzopredsuc  47300  elsprel  47437  clnbgrval  47784  dfvopnbgr2  47814  vopnbgrel  47815  dfclnbgr6  47817  dfnbgr6  47818  cycl3grtri  47907  dmmpossx2  48260  lindslinindsimp2  48387  ldepspr  48397  ldepsnlinc  48432  line  48660  rrxline  48662  dftpos5  48797  tposideq  48811  setc2othin  49300  functermceu  49343  idfudiag1  49358  mndtcval  49404  mndtcbas  49406