Theorem sneqd 4596

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-sn 4585

This theorem is used by:  eqsnuniex  5323  otsndisj  5492  otiunsndisj  5493  iunopeqop  5494  iunopeqopOLD  5495  dmsnopss  6215  dmsnsnsn  6221  opswap  6230  ressn  6288  suceqd  6430  f1osng  6867  fsng  7138  fsn2g  7139  funopsn  7151  funopsnOLD  7152  funsneqopb  7156  fnressn  7162  2nd1st  8049  dfmpo  8113  cnvf1olem  8121  xpord2pred  8162  xpord3pred  8169  suppsnop  8195  tpostpos  8263  tfrlem11  8396  naddcllem  8685  ralxpmap  8924  elixpsn  8965  ixpsnf1o  8966  en1b  9052  mapsnend  9064  xpassen  9090  dif1en  9177  en1eqsn  9266  cantnfp1lem3  9681  axdc4lem  10533  ttukeylem3  10589  ttukey2g  10594  fpwwe2lem12  10727  indval2  12325  fztp  13714  fzsuc2  13716  fseq1p1m1  13732  fseq1m1p1  13733  expval  14206  hash1elsn  14515  s1val  14745  s1eq  14747  s3sndisj  15120  s3iunsndisj  15121  fsumm1  15917  fprodm1  16134  divalgmod  16576  vdwpc  17158  vdwlem1  17159  vdwlem6  17164  vdwlem7  17165  vdwlem8  17166  cshwsdisj  17276  strle1  17336  setsvalg  17344  setsidvald  17377  imasval  17683  imasaddvallem  17701  imasvscaval  17710  ismri2dad  17811  mreexd  17816  mreexmrid  17817  homaval  18206  setcmon  18262  funcsetcestrclem1  18328  chnccats1  18799  chnccat  18800  gsumress  18871  pwsco2mhm  19029  efmnd  19066  idressubmefmnd  19094  smndex1igid  19102  smndex1igidOLD  19103  smndex1basss  19104  smndex1mgm  19106  smndex1mndlem  19108  mulgval  19281  idressubgsymg  19624  gsumzaddlem  20135  dmdprd  20214  subgdmdprd  20250  dprdsn  20252  dprd2da  20258  dmdprdpr  20265  dprdpr  20266  dpjfval  20271  dpjval  20272  ablfac1eulem  20288  pgpfaclem1  20297  isunit  20603  isdrng  20984  drngprop  20998  isdrngd  21022  isdrngdOLD  21024  drngpropd  21027  issubdrg  21037  subdrgint  21060  lspsnneg  21281  lspsnsub  21282  lmodindp1  21289  islbs  21351  lspsntrim  21373  lbspropd  21374  lspsnvs  21392  lspsneleq  21393  lspfixed  21406  rngqiprngimf1  21596  qsidomlem2  21637  lpival  21648  pzriprnglem13  21799  pzriprnglem14  21800  zrhrhmb  21816  znval  21841  isobs  22026  frlmval  22054  frlmlbs  22103  islindf  22118  lindfmm  22133  lsslindf  22136  islindf4  22144  islindf5  22145  psrval  22223  mat1dimmul  22791  mat1dimcrng  22792  mat1rhmval  22794  mat1ric  22802  mat1scmat  22854  mdet0pr  22907  m1detdiag  22912  matunitlindflem1  22994  pmatcoe1fsupp  23019  ordtval  23507  ordtcnv  23519  dissnlocfin  23848  ptval2  23920  dfac14  23937  txdis  23951  xkoptsub  23973  pt1hmeo  24125  xpstopnlem1  24128  tgptsmscls  24469  ustuqtoplem  24558  utopsnneiplem  24566  utopsnneip  24567  utop2nei  24569  utop3cls  24570  pcorev2  25349  pcophtb  25350  pi1grplem  25370  pi1inv  25373  cvsunit  25452  i1f1  26011  i1faddlem  26014  i1fmullem  26015  i1fadd  26016  limcfval  26192  dvnfval  26242  ig1pval  26494  0dgrb  26565  dgrnznn  26566  dgreq0  26584  dgrmulc  26590  plyrem  26626  facth  26627  fta1  26629  aaliou2  26667  taylpfval  26692  nosupbnd2lem1  28072  nosupbnd2  28073  noinfbnd2lem1  28087  noinfbnd2  28088  eqcuts3  28190  addsproplem3  28357  addsuniflem  28387  negsproplem3  28416  negsunif  28441  mulsproplem10  28511  mulsuniflem  28535  n0cut  28720  n0cut2  28721  n0fincut  28741  zcuts  28793  halfcut  28844  addhalfcut  28845  pw2cut  28846  pw2cutp1  28847  pw2cut2  28848  bdaypw2n0bndlem  28849  bdayfinbndlem1  28853  elreno2  28881  axlowdimlem15  29534  axlowdim  29539  1loopgruspgr  30081  1egrvtxdg1r  30091  1egrvtxdg0  30092  wkslem1  30188  wkslem2  30189  iswlk  30191  redwlk  30251  wlkp1lem8  30259  revwlk  30267  crctcshwlkn0lem4  30402  crctcshwlkn0lem5  30403  crctcshwlkn0lem6  30404  loopclwwlkn1b  30633  clwwlkn1loopb  30634  clwwlknon1  30688  eupth2lem3lem3  30831  frgrncvvdeqlem3  30902  frgrncvvdeqlem5  30904  wlkl0  30968  0ofval  31389  fresunsn  33219  fcnvgreu  33266  cycpm2tr  33680  lindfpropd  33937  nsgqusf1olem1  33964  elrspunidl  33978  opprqusdrng  34017  rprmval  34048  isufd  34072  pidufd  34075  r1pquslmic  34142  selvply1rhmlema  34150  selvply1rhmlemb  34151  selvply1rhmlem1  34152  selvply1rhmlem3  34154  selvply1rhmlem5  34156  selvply1rhm  34157  mplidom  34160  extvfvcl  34168  esplyfval0  34196  esplyfval2  34197  esplyind  34207  vieta  34212  sradrng  34214  rlmdim  34242  ply1degltdimlem  34254  dimkerim  34259  lvecendof1f1o  34265  irngval  34317  extdgfialglem1  34324  minplym1p  34345  minplynzm1p  34346  algextdeglem3  34351  algextdeglem4  34352  algextdeglem5  34353  dispcmp  34491  ordtprsval  34550  ordtprsuni  34551  sitgval  34964  sseqval  35020  reprsuc  35244  lpadval  35308  bnj941  35403  bnj944  35568  subfacp1lem5  35949  sconnpht  35994  sconnpht2  36003  sconnpi1  36004  cvmliftlem7  36056  cvmliftlem10  36059  cvmlift2lem13  36080  cvmlift3lem9  36092  satffunlem1lem1  36167  satffunlem2lem1  36169  msrval  36303  mthmpps  36347  onint1  37237  bj-projeq  37905  bj-restsn  38003  finixpnum  38528  ptrest  38537  poimirlem4  38542  poimirlem13  38551  poimirlem14  38552  poimirlem16  38554  poimirlem19  38557  poimirlem26  38564  grpokerinj  38827  isdivrngo  38884  drngoi  38885  isprrngo  38984  lsatset  40047  lsmsat  40065  islshpat  40074  lflsc0N  40140  lkrfval  40144  ldualset  40182  dvafset  42061  dvaset  42062  dvhfset  42137  dvhset  42138  dibffval  42197  dibfval  42198  dib0  42221  cdlemn4a  42256  dihmeetlem4preN  42363  dihmeetlem13N  42376  dih1dimatlem  42386  dihlsprn  42388  dvh2dim  42502  lpolsetN  42539  lclkrlem2j  42573  lclkrlem2p  42579  lcfrlem21  42620  mapdpglem22  42750  mapdpglem23  42751  mapdpglem26  42755  mapdpglem27  42756  mapdpg  42763  baerlem3lem2  42767  baerlem5alem2  42768  baerlem5blem2  42769  baerlem5amN  42773  baerlem5bmN  42774  baerlem5abmN  42775  mapdindp4  42780  mapdhval  42781  mapdheq  42785  mapdh6aN  42792  hvmapffval  42815  hvmapfval  42816  hvmap1o2  42822  hdmap1fval  42853  hdmap1vallem  42854  hdmap1val  42855  hdmap1eq  42858  hdmap1cbv  42859  hdmap1l6a  42866  hdmapfval  42884  hdmap10  42897  hdmaprnlem6N  42911  hgmaprnlem2N  42954  lcmfunnnd  43062  aks6d1c6lem5  43227  qsalrel  43292  frlmsnic  43604  prjspval  43631  prjspval2  43641  prjspnvs  43648  prjcrvfval  43667  dfac11  44063  dfac21  44067  nzprmdif  45302  expgrowth  45318  fzdifsuc2  46325  cnrefiisplem  46838  cnrefiisp  46839  hoidmv1le  47603  ovnovollem3  47667  fsetsniunop  48118  fsetsnf  48120  fsetsnf1  48121  fsetsnfo  48122  dfateq12d  48195  otiunsndisjX  48348  funop1  48352  preimafvelsetpreimafv  48469  imaelsetpreimafv  48476  imasetpreimafvbijlemfo  48486  fundcmpsurbijinjpreimafv  48488  fundcmpsurinj  48490  fundcmpsurbijinj  48491  isprmrng  49432  lmod1zr  49604  0aryfvalel  49745  1arymaptf1  49753  discsubc  50171  imasubclem3  50213  swapf1a  50376  swapf2a  50378  swapf1  50379  swapf2  50381  termcbas2  50589  termchom  50595  termchom2  50596  termcfuncval  50639  mndtcval  50686