Theorem sneqd 4660

Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)

Hypothesis

Ref	Expression
sneqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sneqd	⊢ (𝜑 → {𝐴} = {𝐵})

Proof of Theorem sneqd

Step	Hyp	Ref	Expression
1		sneqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sneq 4658	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1537  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-sn 4649

This theorem is referenced by:  eqsnuniex  5379  otsndisj  5538  otiunsndisj  5539  iunopeqop  5540  dmsnopss  6245  dmsnsnsn  6251  opswap  6260  ressn  6316  f1osng  6903  fsng  7171  fsn2g  7172  funopsn  7182  funsneqopb  7186  fnressn  7192  2nd1st  8079  dfmpo  8143  cnvf1olem  8151  xpord2pred  8186  xpord3pred  8193  suppsnop  8219  tpostpos  8287  tfrlem11  8444  naddcllem  8732  ralxpmap  8954  elixpsn  8995  ixpsnf1o  8996  en1b  9088  en1bOLD  9089  mapsnend  9101  xpassen  9132  dif1en  9226  dif1enOLD  9228  en1eqsn  9336  cantnfp1lem3  9749  axdc4lem  10524  ttukeylem3  10580  ttukey2g  10585  fpwwe2lem12  10711  fztp  13640  fzsuc2  13642  fseq1p1m1  13658  fseq1m1p1  13659  expval  14114  hash1elsn  14420  s1val  14646  s1eq  14648  s3sndisj  15016  s3iunsndisj  15017  fsumm1  15799  fprodm1  16015  divalgmod  16454  vdwpc  17027  vdwlem1  17028  vdwlem6  17033  vdwlem7  17034  vdwlem8  17035  cshwsdisj  17146  strle1  17205  setsvalg  17213  setsidvald  17246  setsidvaldOLD  17247  imasval  17571  imasaddvallem  17589  imasvscaval  17598  ismri2dad  17695  mreexd  17700  mreexmrid  17701  homaval  18098  setcmon  18154  funcsetcestrclem1  18223  gsumress  18720  pwsco2mhm  18868  efmnd  18905  idressubmefmnd  18933  smndex1igid  18939  smndex1basss  18940  smndex1mgm  18942  smndex1mndlem  18944  mulgval  19111  idressubgsymg  19452  gsumzaddlem  19963  dmdprd  20042  subgdmdprd  20078  dprdsn  20080  dprd2da  20086  dmdprdpr  20093  dprdpr  20094  dpjfval  20099  dpjval  20100  ablfac1eulem  20116  pgpfaclem1  20125  isunit  20399  isdrng  20755  drngprop  20766  isdrngd  20787  isdrngdOLD  20789  drngpropd  20791  issubdrg  20803  subdrgint  20826  lspsnneg  21027  lspsnsub  21028  lmodindp1  21035  islbs  21098  lspsntrim  21120  lbspropd  21121  lspsnvs  21139  lspsneleq  21140  lspfixed  21153  rngqiprngimf1  21333  lpival  21357  pzriprnglem13  21527  pzriprnglem14  21528  zrhrhmb  21544  znval  21573  isobs  21763  frlmval  21791  frlmlbs  21840  islindf  21855  lindfmm  21870  lsslindf  21873  islindf4  21881  islindf5  21882  psrval  21958  mat1dimmul  22503  mat1dimcrng  22504  mat1rhmval  22506  mat1ric  22514  mat1scmat  22566  mdet0pr  22619  m1detdiag  22624  pmatcoe1fsupp  22728  ordtval  23218  ordtcnv  23230  dissnlocfin  23558  ptval2  23630  dfac14  23647  txdis  23661  xkoptsub  23683  pt1hmeo  23835  xpstopnlem1  23838  tgptsmscls  24179  ustuqtoplem  24269  utopsnneiplem  24277  utopsnneip  24278  utop2nei  24280  utop3cls  24281  pcorev2  25080  pcophtb  25081  pi1grplem  25101  pi1inv  25104  cvsunit  25183  i1f1  25744  i1faddlem  25747  i1fmullem  25748  i1fadd  25749  limcfval  25927  dvnfval  25978  ig1pval  26235  0dgrb  26305  dgrnznn  26306  dgreq0  26325  dgrmulc  26331  plyrem  26365  facth  26366  fta1  26368  aaliou2  26400  taylpfval  26424  nosupbnd2lem1  27778  nosupbnd2  27779  noinfbnd2lem1  27793  noinfbnd2  27794  addsproplem3  28022  addsuniflem  28052  negsproplem3  28080  negsunif  28105  mulsproplem10  28169  mulsuniflem  28193  n0scut  28356  n0sbday  28372  zscut  28411  halfcut  28434  cutpw2  28435  addhalfcut  28437  pw2cut  28438  zs12bday  28442  axlowdimlem15  28989  axlowdim  28994  1loopgruspgr  29536  1egrvtxdg1r  29546  1egrvtxdg0  29547  wkslem1  29643  wkslem2  29644  iswlk  29646  redwlk  29708  wlkp1lem8  29716  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  crctcshwlkn0lem6  29848  loopclwwlkn1b  30074  clwwlkn1loopb  30075  clwwlknon1  30129  eupth2lem3lem3  30262  frgrncvvdeqlem3  30333  frgrncvvdeqlem5  30335  wlkl0  30399  0ofval  30819  fcnvgreu  32691  cycpm2tr  33112  lindfpropd  33375  nsgqusf1olem1  33406  elrspunidl  33421  qsidomlem2  33446  opprqusdrng  33486  rprmval  33509  isufd  33533  pidufd  33536  r1pquslmic  33596  sradrng  33598  rlmdim  33622  rgmoddimOLD  33623  ply1degltdimlem  33635  dimkerim  33640  lvecendof1f1o  33646  irngval  33685  minplym1p  33706  algextdeglem3  33710  algextdeglem4  33711  algextdeglem5  33712  dispcmp  33805  ordtprsval  33864  ordtprsuni  33865  indval2  33978  sitgval  34297  sseqval  34353  reprsuc  34592  lpadval  34653  bnj941  34748  bnj944  34914  revwlk  35092  subfacp1lem5  35152  sconnpht  35197  sconnpht2  35206  sconnpi1  35207  cvmliftlem7  35259  cvmliftlem10  35262  cvmlift2lem13  35283  cvmlift3lem9  35295  satffunlem1lem1  35370  satffunlem2lem1  35372  msrval  35506  mthmpps  35550  onint1  36415  bj-projeq  36958  bj-restsn  37048  finixpnum  37565  matunitlindflem1  37576  ptrest  37579  poimirlem4  37584  poimirlem13  37593  poimirlem14  37594  poimirlem16  37596  poimirlem19  37599  poimirlem26  37606  grpokerinj  37853  isdivrngo  37910  drngoi  37911  isprrngo  38010  lsatset  38946  lsmsat  38964  islshpat  38973  lflsc0N  39039  lkrfval  39043  ldualset  39081  dvafset  40961  dvaset  40962  dvhfset  41037  dvhset  41038  dibffval  41097  dibfval  41098  dib0  41121  cdlemn4a  41156  dihmeetlem4preN  41263  dihmeetlem13N  41276  dih1dimatlem  41286  dihlsprn  41288  dvh2dim  41402  lpolsetN  41439  lclkrlem2j  41473  lclkrlem2p  41479  lcfrlem21  41520  mapdpglem22  41650  mapdpglem23  41651  mapdpglem26  41655  mapdpglem27  41656  mapdpg  41663  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  baerlem5amN  41673  baerlem5bmN  41674  baerlem5abmN  41675  mapdindp4  41680  mapdhval  41681  mapdheq  41685  mapdh6aN  41692  hvmapffval  41715  hvmapfval  41716  hvmap1o2  41722  hdmap1fval  41753  hdmap1vallem  41754  hdmap1val  41755  hdmap1eq  41758  hdmap1cbv  41759  hdmap1l6a  41766  hdmapfval  41784  hdmap10  41797  hdmaprnlem6N  41811  hgmaprnlem2N  41854  lcmfunnnd  41969  aks6d1c6lem5  42134  qsalrel  42235  frlmsnic  42495  prjspval  42558  prjspval2  42568  prjspnvs  42575  prjcrvfval  42586  dfac11  43019  dfac21  43023  nzprmdif  44288  expgrowth  44304  fzdifsuc2  45225  cnrefiisplem  45750  cnrefiisp  45751  hoidmv1le  46515  ovnovollem3  46579  fsetsniunop  46964  fsetsnf  46966  fsetsnf1  46967  fsetsnfo  46968  dfateq12d  47041  otiunsndisjX  47194  funop1  47198  preimafvelsetpreimafv  47262  imaelsetpreimafv  47269  imasetpreimafvbijlemfo  47279  fundcmpsurbijinjpreimafv  47281  fundcmpsurinj  47283  fundcmpsurbijinj  47284  lmod1zr  48222  0aryfvalel  48368  1arymaptf1  48376  mndtcval  48752