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 4588

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-sn 4589

This theorem is used by:  eqsnuniex  5330  otsndisj  5499  otiunsndisj  5500  iunopeqop  5501  iunopeqopOLD  5502  dmsnopss  6234  dmsnsnsn  6240  opswap  6249  ressn  6312  suceqd  6456  f1osng  6898  fsng  7170  fsn2g  7171  funopsn  7183  funopsnOLD  7184  funsneqopb  7188  fnressn  7194  2nd1st  8083  dfmpo  8150  cnvf1olem  8158  xpord2pred  8199  xpord3pred  8206  suppsnop  8233  tpostpos  8301  tfrlem11  8434  naddcllem  8723  ralxpmap  8962  elixpsn  9003  ixpsnf1o  9004  en1b  9090  mapsnend  9102  xpassen  9128  dif1en  9215  en1eqsn  9304  cantnfp1lem3  9718  axdc4lem  10572  ttukeylem3  10628  ttukey2g  10633  fpwwe2lem12  10766  indval2  12365  fztp  13754  fzsuc2  13756  fseq1p1m1  13772  fseq1m1p1  13773  expval  14246  hash1elsn  14556  s1val  14786  s1eq  14788  s3sndisj  15163  s3iunsndisj  15164  fsumm1  15961  fprodm1  16178  divalgmod  16620  vdwpc  17202  vdwlem1  17203  vdwlem6  17208  vdwlem7  17209  vdwlem8  17210  cshwsdisj  17320  strle1  17380  setsvalg  17388  setsidvald  17421  imasval  17733  imasaddvallem  17751  imasvscaval  17760  ismri2dad  17861  mreexd  17866  mreexmrid  17867  homaval  18256  setcmon  18312  funcsetcestrclem1  18378  chnccats1  18849  chnccat  18850  gsumress  18921  pwsco2mhm  19079  efmnd  19116  idressubmefmnd  19144  smndex1igid  19152  smndex1igidOLD  19153  smndex1basss  19154  smndex1mgm  19156  smndex1mndlem  19158  mulgval  19331  idressubgsymg  19675  gsumzaddlem  20186  dmdprd  20265  subgdmdprd  20301  dprdsn  20303  dprd2da  20309  dmdprdpr  20316  dprdpr  20317  dpjfval  20322  dpjval  20323  ablfac1eulem  20339  pgpfaclem1  20348  isunit  20654  isdrng  21035  drngprop  21049  isdrngd  21073  isdrngdOLD  21075  drngpropd  21078  issubdrg  21088  subdrgint  21111  lspsnneg  21332  lspsnsub  21333  lmodindp1  21340  islbs  21402  lspsntrim  21424  lbspropd  21425  lspsnvs  21443  lspsneleq  21444  lspfixed  21457  rngqiprngimf1  21647  qsidomlem2  21688  lpival  21699  pzriprnglem13  21854  pzriprnglem14  21855  zrhrhmb  21871  znval  21896  isobs  22081  frlmval  22109  frlmlbs  22158  islindf  22173  lindfmm  22188  lsslindf  22191  islindf4  22199  islindf5  22200  psrval  22278  mat1dimmul  22846  mat1dimcrng  22847  mat1rhmval  22849  mat1ric  22857  mat1scmat  22909  mdet0pr  22962  m1detdiag  22967  matunitlindflem1  23049  pmatcoe1fsupp  23074  ordtval  23562  ordtcnv  23574  dissnlocfin  23903  ptval2  23975  dfac14  23992  txdis  24006  xkoptsub  24028  pt1hmeo  24180  xpstopnlem1  24183  tgptsmscls  24524  ustuqtoplem  24613  utopsnneiplem  24621  utopsnneip  24622  utop2nei  24624  utop3cls  24625  pcorev2  25404  pcophtb  25405  pi1grplem  25425  pi1inv  25428  cvsunit  25507  i1f1  26066  i1faddlem  26069  i1fmullem  26070  i1fadd  26071  limcfval  26247  dvnfval  26297  ig1pval  26549  0dgrb  26620  dgrnznn  26621  dgreq0  26639  dgrmulc  26645  plyrem  26681  facth  26682  fta1  26684  aaliou2  26724  taylpfval  26749  nosupbnd2lem1  28129  nosupbnd2  28130  noinfbnd2lem1  28144  noinfbnd2  28145  eqcuts3  28247  addsproplem3  28414  addsuniflem  28444  negsproplem3  28473  negsunif  28498  mulsproplem10  28568  mulsuniflem  28592  n0cut  28777  n0cut2  28778  n0fincut  28798  zcuts  28850  halfcut  28901  addhalfcut  28902  pw2cut  28903  pw2cutp1  28904  pw2cut2  28905  bdaypw2n0bndlem  28906  bdayfinbndlem1  28910  elreno2  28938  axlowdimlem15  29591  axlowdim  29596  1loopgruspgr  30138  1egrvtxdg1r  30148  1egrvtxdg0  30149  wkslem1  30245  wkslem2  30246  iswlk  30248  redwlk  30308  wlkp1lem8  30316  revwlk  30324  crctcshwlkn0lem4  30459  crctcshwlkn0lem5  30460  crctcshwlkn0lem6  30461  loopclwwlkn1b  30690  clwwlkn1loopb  30691  clwwlknon1  30745  eupth2lem3lem3  30888  frgrncvvdeqlem3  30959  frgrncvvdeqlem5  30961  wlkl0  31025  0ofval  31446  fresunsn  33317  fcnvgreu  33364  cycpm2tr  33779  isedom  33953  lindfpropd  34041  nsgqusf1olem1  34068  elrspunidl  34082  opprqusdrng  34121  rprmval  34152  isufd  34176  pidufd  34179  r1pquslmic  34247  selvply1rhmlema  34261  selvply1rhmlemb  34262  selvply1rhmlem1  34263  selvply1rhmlem3  34265  selvply1rhmlem5  34267  selvply1rhm  34268  mplidom  34271  extvfvcl  34279  esplyfval0  34307  esplyfval2  34308  esplyind  34318  vieta  34323  sradrng  34325  rlmdim  34353  ply1degltdimlem  34365  dimkerim  34370  lvecendof1f1o  34376  irngval  34428  extdgfialglem1  34435  minplym1p  34456  minplynzm1p  34457  algextdeglem3  34462  algextdeglem4  34463  algextdeglem5  34464  dispcmp  34602  ordtprsval  34661  ordtprsuni  34662  sitgval  35075  sseqval  35131  reprsuc  35355  lpadval  35419  bnj941  35514  bnj944  35679  subfacp1lem5  36157  sconnpht  36202  sconnpht2  36211  sconnpi1  36212  cvmliftlem7  36264  cvmliftlem10  36267  cvmlift2lem13  36288  cvmlift3lem9  36300  satffunlem1lem1  36375  satffunlem2lem1  36377  msrval  36511  mthmpps  36555  onint1  37452  bj-projeq  38120  bj-restsn  38273  finixpnum  38796  ptrest  38805  poimirlem4  38810  poimirlem13  38819  poimirlem14  38820  poimirlem16  38822  poimirlem19  38825  poimirlem26  38832  grpokerinj  39093  isdivrngo  39150  drngoi  39151  isprrngo  39250  lsatset  40313  lsmsat  40331  islshpat  40340  lflsc0N  40406  lkrfval  40410  ldualset  40448  dvafset  42327  dvaset  42328  dvhfset  42403  dvhset  42404  dibffval  42463  dibfval  42464  dib0  42487  cdlemn4a  42522  dihmeetlem4preN  42629  dihmeetlem13N  42642  dih1dimatlem  42652  dihlsprn  42654  dvh2dim  42768  lpolsetN  42805  lclkrlem2j  42839  lclkrlem2p  42845  lcfrlem21  42886  mapdpglem22  43016  mapdpglem23  43017  mapdpglem26  43021  mapdpglem27  43022  mapdpg  43029  baerlem3lem2  43033  baerlem5alem2  43034  baerlem5blem2  43035  baerlem5amN  43039  baerlem5bmN  43040  baerlem5abmN  43041  mapdindp4  43046  mapdhval  43047  mapdheq  43051  mapdh6aN  43058  hvmapffval  43081  hvmapfval  43082  hvmap1o2  43088  hdmap1fval  43119  hdmap1vallem  43120  hdmap1val  43121  hdmap1eq  43124  hdmap1cbv  43125  hdmap1l6a  43132  hdmapfval  43150  hdmap10  43163  hdmaprnlem6N  43177  hgmaprnlem2N  43220  lcmfunnnd  43328  aks6d1c6lem5  43493  qsalrel  43559  frlmsnic  43870  prjspval  43897  prjspval2  43907  prjspnvs  43914  prjcrvfval  43933  dfac11  44330  dfac21  44334  nzprmdif  45564  expgrowth  45580  fzdifsuc2  46599  cnrefiisplem  47112  cnrefiisp  47113  hoidmv1le  47877  ovnovollem3  47941  fsetsniunop  48392  fsetsnf  48394  fsetsnf1  48395  fsetsnfo  48396  dfateq12d  48469  otiunsndisjX  48622  funop1  48626  preimafvelsetpreimafv  48743  imaelsetpreimafv  48750  imasetpreimafvbijlemfo  48760  fundcmpsurbijinjpreimafv  48762  fundcmpsurinj  48764  fundcmpsurbijinj  48765  isprmrng  49764  lmod1zr  49936  0aryfvalel  50077  1arymaptf1  50085  discsubc  50509  imasubclem3  50553  swapf1a  50722  swapf2a  50724  swapf1  50725  swapf2  50727  termcbas2  50948  termchom  50954  termchom2  50955  termcfuncval  50998  termcfunc1eq  51001  mndtcval  51048