Theorem sneqd 4535

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

Syntax hints:   → wi 4   = wceq 1539  {csn 4523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-sn 4524

This theorem is referenced by:  otsndisj  5379  otiunsndisj  5380  iunopeqop  5381  dmsnopss  6044  dmsnsnsn  6050  opswap  6059  ressn  6115  f1osng  6643  fsng  6891  fsn2g  6892  funopsn  6902  funsneqopb  6906  fnressn  6912  2nd1st  7742  dfmpo  7803  cnvf1olem  7811  suppsnop  7853  tpostpos  7923  tfrlem11  8035  ralxpmap  8479  elixpsn  8520  ixpsnf1o  8521  en1b  8597  mapsnend  8608  xpassen  8633  dif1en  8734  cantnfp1lem3  9177  axdc4lem  9916  ttukeylem3  9972  ttukey2g  9977  fpwwe2lem12  10103  fztp  13013  fzsuc2  13015  fseq1p1m1  13031  fseq1m1p1  13032  expval  13482  hash1elsn  13783  s1val  14000  s1eq  14002  s3sndisj  14375  s3iunsndisj  14376  fsumm1  15155  fprodm1  15370  divalgmod  15808  vdwpc  16372  vdwlem1  16373  vdwlem6  16378  vdwlem7  16379  vdwlem8  16380  cshwsdisj  16491  setsvalg  16571  setsidvald  16573  strle1  16651  imasval  16843  imasaddvallem  16861  imasvscaval  16870  ismri2dad  16967  mreexd  16972  mreexmrid  16973  homaval  17358  setcmon  17414  funcsetcestrclem1  17471  gsumress  17959  pwsco2mhm  18064  efmnd  18102  idressubmefmnd  18130  smndex1igid  18136  smndex1basss  18137  smndex1mgm  18139  smndex1mndlem  18141  mulgval  18296  idressubgsymg  18606  gsumzaddlem  19110  dmdprd  19189  subgdmdprd  19225  dprdsn  19227  dprd2da  19233  dmdprdpr  19240  dprdpr  19241  dpjfval  19246  dpjval  19247  ablfac1eulem  19263  pgpfaclem1  19272  isunit  19479  isdrng  19575  drngprop  19582  isdrngd  19596  drngpropd  19598  issubdrg  19629  subdrgint  19651  lspsnneg  19847  lspsnsub  19848  lmodindp1  19855  islbs  19917  lspsntrim  19939  lbspropd  19940  lspsnvs  19955  lspsneleq  19956  lspfixed  19969  lpival  20087  zrhrhmb  20281  znval  20304  isobs  20486  frlmval  20514  frlmlbs  20563  islindf  20578  lindfmm  20593  lsslindf  20596  islindf4  20604  islindf5  20605  psrval  20678  mat1dimmul  21177  mat1dimcrng  21178  mat1rhmval  21180  mat1ric  21188  mat1scmat  21240  mdet0pr  21293  m1detdiag  21298  pmatcoe1fsupp  21402  ordtval  21890  ordtcnv  21902  dissnlocfin  22230  ptval2  22302  dfac14  22319  txdis  22333  xkoptsub  22355  pt1hmeo  22507  xpstopnlem1  22510  tgptsmscls  22851  ustuqtoplem  22941  utopsnneiplem  22949  utopsnneip  22950  utop2nei  22952  utop3cls  22953  pcorev2  23730  pcophtb  23731  pi1grplem  23751  pi1inv  23754  cvsunit  23833  i1f1  24391  i1faddlem  24394  i1fmullem  24395  i1fadd  24396  limcfval  24572  dvnfval  24622  ig1pval  24873  0dgrb  24943  dgrnznn  24944  dgreq0  24962  dgrmulc  24968  plyrem  25001  facth  25002  fta1  25004  aaliou2  25036  taylpfval  25060  axlowdimlem15  26850  axlowdim  26855  1loopgruspgr  27390  1egrvtxdg1r  27400  1egrvtxdg0  27401  wkslem1  27497  wkslem2  27498  iswlk  27500  redwlk  27562  wlkp1lem8  27570  crctcshwlkn0lem4  27699  crctcshwlkn0lem5  27700  crctcshwlkn0lem6  27701  loopclwwlkn1b  27927  clwwlkn1loopb  27928  clwwlknon1  27982  eupth2lem3lem3  28115  frgrncvvdeqlem3  28186  frgrncvvdeqlem5  28188  wlkl0  28252  0ofval  28670  fcnvgreu  30535  cycpm2tr  30913  lindfpropd  31098  nsgqusf1olem1  31120  elrspunidl  31128  qsidomlem2  31151  rprmval  31186  sradrng  31195  rgmoddim  31215  dimkerim  31230  dispcmp  31331  ordtprsval  31390  ordtprsuni  31391  indval2  31502  sitgval  31819  sseqval  31875  reprsuc  32115  lpadval  32176  bnj941  32273  bnj944  32439  revwlk  32603  subfacp1lem5  32663  sconnpht  32708  sconnpht2  32717  sconnpi1  32718  cvmliftlem7  32770  cvmliftlem10  32773  cvmlift2lem13  32794  cvmlift3lem9  32806  satffunlem1lem1  32881  satffunlem2lem1  32883  msrval  33017  mthmpps  33061  xpord2pred  33348  xpord3pred  33354  nosupbnd2lem1  33484  nosupbnd2  33485  noinfbnd2lem1  33499  noinfbnd2  33500  onint1  34188  bj-projeq  34710  bj-restsn  34778  finixpnum  35323  matunitlindflem1  35334  ptrest  35337  poimirlem4  35342  poimirlem13  35351  poimirlem14  35352  poimirlem16  35354  poimirlem19  35357  poimirlem26  35364  grpokerinj  35612  isdivrngo  35669  drngoi  35670  isprrngo  35769  lsatset  36567  lsmsat  36585  islshpat  36594  lflsc0N  36660  lkrfval  36664  ldualset  36702  dvafset  38581  dvaset  38582  dvhfset  38657  dvhset  38658  dibffval  38717  dibfval  38718  dib0  38741  cdlemn4a  38776  dihmeetlem4preN  38883  dihmeetlem13N  38896  dih1dimatlem  38906  dihlsprn  38908  dvh2dim  39022  lpolsetN  39059  lclkrlem2j  39093  lclkrlem2p  39099  lcfrlem21  39140  mapdpglem22  39270  mapdpglem23  39271  mapdpglem26  39275  mapdpglem27  39276  mapdpg  39283  baerlem3lem2  39287  baerlem5alem2  39288  baerlem5blem2  39289  baerlem5amN  39293  baerlem5bmN  39294  baerlem5abmN  39295  mapdindp4  39300  mapdhval  39301  mapdheq  39305  mapdh6aN  39312  hvmapffval  39335  hvmapfval  39336  hvmap1o2  39342  hdmap1fval  39373  hdmap1vallem  39374  hdmap1val  39375  hdmap1eq  39378  hdmap1cbv  39379  hdmap1l6a  39386  hdmapfval  39404  hdmap10  39417  hdmaprnlem6N  39431  hgmaprnlem2N  39474  lcmfunnnd  39580  qsalrel  39722  frlmsnic  39771  evlsbagval  39781  prjspval  39940  prjspval2  39950  prjspnvs  39957  dfac11  40380  dfac21  40384  nzprmdif  41397  expgrowth  41413  fzdifsuc2  42311  cnrefiisplem  42838  cnrefiisp  42839  hoidmv1le  43600  ovnovollem3  43664  dfateq12d  44051  otiunsndisjX  44204  funop1  44208  preimafvelsetpreimafv  44274  imaelsetpreimafv  44281  imasetpreimafvbijlemfo  44291  fundcmpsurbijinjpreimafv  44293  fundcmpsurinj  44295  fundcmpsurbijinj  44296  lmod1zr  45268  0aryfvalel  45414  1arymaptf1  45422