Theorem sneqd 4594

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 4592	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴} = {𝐵})

Syntax hints:   → wi 4   = wceq 1560  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-sn 4583

This theorem is referenced by:  eqsnuniex  5318  otsndisj  5488  otiunsndisj  5489  iunopeqop  5490  iunopeqopOLD  5491  dmsnopss  6201  dmsnsnsn  6207  opswap  6216  ressn  6272  suceqd  6413  f1osng  6849  fsng  7119  fsn2g  7120  funopsn  7130  funopsnOLD  7131  funsneqopb  7135  fnressn  7141  2nd1st  8019  dfmpo  8081  cnvf1olem  8089  xpord2pred  8125  xpord3pred  8132  suppsnop  8158  tpostpos  8226  tfrlem11  8359  naddcllem  8646  ralxpmap  8878  elixpsn  8919  ixpsnf1o  8920  en1b  9006  mapsnend  9017  xpassen  9043  dif1en  9130  en1eqsn  9219  cantnfp1lem3  9635  axdc4lem  10412  ttukeylem3  10468  ttukey2g  10473  fpwwe2lem12  10600  indval2  12200  fztp  13585  fzsuc2  13587  fseq1p1m1  13603  fseq1m1p1  13604  expval  14076  hash1elsn  14384  s1val  14612  s1eq  14614  s3sndisj  14980  s3iunsndisj  14981  fsumm1  15778  fprodm1  15997  divalgmod  16440  vdwpc  17016  vdwlem1  17017  vdwlem6  17022  vdwlem7  17023  vdwlem8  17024  cshwsdisj  17134  strle1  17194  setsvalg  17202  setsidvald  17235  imasval  17541  imasaddvallem  17559  imasvscaval  17568  ismri2dad  17669  mreexd  17674  mreexmrid  17675  homaval  18064  setcmon  18120  funcsetcestrclem1  18186  chnccats1  18657  chnccat  18658  gsumress  18716  pwsco2mhm  18867  efmnd  18904  idressubmefmnd  18932  smndex1igid  18940  smndex1igidOLD  18941  smndex1basss  18942  smndex1mgm  18944  smndex1mndlem  18946  mulgval  19113  idressubgsymg  19450  gsumzaddlem  19961  dmdprd  20040  subgdmdprd  20076  dprdsn  20078  dprd2da  20084  dmdprdpr  20091  dprdpr  20092  dpjfval  20097  dpjval  20098  ablfac1eulem  20114  pgpfaclem1  20123  isunit  20422  isdrng  20783  drngprop  20794  isdrngd  20815  isdrngdOLD  20817  drngpropd  20819  issubdrg  20829  subdrgint  20852  lspsnneg  21073  lspsnsub  21074  lmodindp1  21081  islbs  21143  lspsntrim  21165  lbspropd  21166  lspsnvs  21184  lspsneleq  21185  lspfixed  21198  rngqiprngimf1  21370  lpival  21394  pzriprnglem13  21545  pzriprnglem14  21546  zrhrhmb  21562  znval  21587  isobs  21772  frlmval  21800  frlmlbs  21849  islindf  21864  lindfmm  21879  lsslindf  21882  islindf4  21890  islindf5  21891  psrval  21967  mat1dimmul  22536  mat1dimcrng  22537  mat1rhmval  22539  mat1ric  22547  mat1scmat  22599  mdet0pr  22652  m1detdiag  22657  pmatcoe1fsupp  22761  ordtval  23249  ordtcnv  23261  dissnlocfin  23589  ptval2  23661  dfac14  23678  txdis  23692  xkoptsub  23714  pt1hmeo  23866  xpstopnlem1  23869  tgptsmscls  24210  ustuqtoplem  24299  utopsnneiplem  24307  utopsnneip  24308  utop2nei  24310  utop3cls  24311  pcorev2  25090  pcophtb  25091  pi1grplem  25111  pi1inv  25114  cvsunit  25193  i1f1  25752  i1faddlem  25755  i1fmullem  25756  i1fadd  25757  limcfval  25934  dvnfval  25984  ig1pval  26236  0dgrb  26306  dgrnznn  26307  dgreq0  26325  dgrmulc  26331  plyrem  26369  facth  26370  fta1  26372  aaliou2  26404  taylpfval  26428  nosupbnd2lem1  27779  nosupbnd2  27780  noinfbnd2lem1  27794  noinfbnd2  27795  eqcuts3  27897  addsproplem3  28064  addsuniflem  28094  negsproplem3  28123  negsunif  28148  mulsproplem10  28218  mulsuniflem  28242  n0cut  28427  n0cut2  28428  n0fincut  28448  zcuts  28500  halfcut  28551  addhalfcut  28552  pw2cut  28553  pw2cutp1  28554  pw2cut2  28555  bdaypw2n0bndlem  28556  bdayfinbndlem1  28560  elreno2  28588  axlowdimlem15  29157  axlowdim  29162  1loopgruspgr  29701  1egrvtxdg1r  29711  1egrvtxdg0  29712  wkslem1  29808  wkslem2  29809  iswlk  29811  redwlk  29871  wlkp1lem8  29879  crctcshwlkn0lem4  30013  crctcshwlkn0lem5  30014  crctcshwlkn0lem6  30015  loopclwwlkn1b  30244  clwwlkn1loopb  30245  clwwlknon1  30299  eupth2lem3lem3  30432  frgrncvvdeqlem3  30503  frgrncvvdeqlem5  30505  wlkl0  30569  0ofval  30990  fresunsn  32827  fcnvgreu  32874  cycpm2tr  33299  lindfpropd  33568  nsgqusf1olem1  33599  elrspunidl  33614  qsidomlem2  33640  opprqusdrng  33681  rprmval  33712  isufd  33736  pidufd  33739  r1pquslmic  33807  selvply1rhmlema  33815  selvply1rhmlemb  33816  selvply1rhmlem1  33817  selvply1rhmlem3  33819  selvply1rhmlem5  33821  selvply1rhm  33822  mplidom  33825  extvfvcl  33833  esplyfval0  33861  esplyfval2  33862  esplyind  33872  vieta  33877  sradrng  33879  rlmdim  33907  ply1degltdimlem  33919  dimkerim  33924  lvecendof1f1o  33930  irngval  33982  extdgfialglem1  33989  minplym1p  34010  minplynzm1p  34011  algextdeglem3  34016  algextdeglem4  34017  algextdeglem5  34018  dispcmp  34156  ordtprsval  34215  ordtprsuni  34216  sitgval  34629  sseqval  34685  reprsuc  34909  lpadval  34973  bnj941  35068  bnj944  35233  revwlk  35475  subfacp1lem5  35534  sconnpht  35579  sconnpht2  35588  sconnpi1  35589  cvmliftlem7  35641  cvmliftlem10  35644  cvmlift2lem13  35665  cvmlift3lem9  35677  satffunlem1lem1  35752  satffunlem2lem1  35754  msrval  35888  mthmpps  35932  onint1  36809  bj-projeq  37477  bj-restsn  37572  finixpnum  38104  matunitlindflem1  38115  ptrest  38118  poimirlem4  38123  poimirlem13  38132  poimirlem14  38133  poimirlem16  38135  poimirlem19  38138  poimirlem26  38145  grpokerinj  38392  isdivrngo  38449  drngoi  38450  isprrngo  38549  lsatset  39614  lsmsat  39632  islshpat  39641  lflsc0N  39707  lkrfval  39711  ldualset  39749  dvafset  41628  dvaset  41629  dvhfset  41704  dvhset  41705  dibffval  41764  dibfval  41765  dib0  41788  cdlemn4a  41823  dihmeetlem4preN  41930  dihmeetlem13N  41943  dih1dimatlem  41953  dihlsprn  41955  dvh2dim  42069  lpolsetN  42106  lclkrlem2j  42140  lclkrlem2p  42146  lcfrlem21  42187  mapdpglem22  42317  mapdpglem23  42318  mapdpglem26  42322  mapdpglem27  42323  mapdpg  42330  baerlem3lem2  42334  baerlem5alem2  42335  baerlem5blem2  42336  baerlem5amN  42340  baerlem5bmN  42341  baerlem5abmN  42342  mapdindp4  42347  mapdhval  42348  mapdheq  42352  mapdh6aN  42359  hvmapffval  42382  hvmapfval  42383  hvmap1o2  42389  hdmap1fval  42420  hdmap1vallem  42421  hdmap1val  42422  hdmap1eq  42425  hdmap1cbv  42426  hdmap1l6a  42433  hdmapfval  42451  hdmap10  42464  hdmaprnlem6N  42478  hgmaprnlem2N  42521  lcmfunnnd  42629  aks6d1c6lem5  42794  qsalrel  42857  frlmsnic  43158  prjspval  43185  prjspval2  43195  prjspnvs  43202  prjcrvfval  43213  dfac11  43639  dfac21  43643  nzprmdif  44895  expgrowth  44911  fzdifsuc2  45889  cnrefiisplem  46403  cnrefiisp  46404  hoidmv1le  47168  ovnovollem3  47232  fsetsniunop  47643  fsetsnf  47645  fsetsnf1  47646  fsetsnfo  47647  dfateq12d  47720  otiunsndisjX  47873  funop1  47877  preimafvelsetpreimafv  47994  imaelsetpreimafv  48001  imasetpreimafvbijlemfo  48011  fundcmpsurbijinjpreimafv  48013  fundcmpsurinj  48015  fundcmpsurbijinj  48016  lmod1zr  49115  0aryfvalel  49256  1arymaptf1  49264  discsubc  49685  imasubclem3  49727  swapf1a  49890  swapf2a  49892  swapf1  49893  swapf2  49895  termcbas2  50103  termchom  50109  termchom2  50110  termcfuncval  50153  mndtcval  50200