Theorem sneqd 4595

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  {csn 4583

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-sn 4584

This theorem is used by:  eqsnuniex  5322  otsndisj  5491  otiunsndisj  5492  iunopeqop  5493  iunopeqopOLD  5494  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  33261  fcnvgreu  33308  cycpm2tr  33722  lindfpropd  33979  nsgqusf1olem1  34006  elrspunidl  34020  opprqusdrng  34059  rprmval  34090  isufd  34114  pidufd  34117  r1pquslmic  34184  selvply1rhmlema  34192  selvply1rhmlemb  34193  selvply1rhmlem1  34194  selvply1rhmlem3  34196  selvply1rhmlem5  34198  selvply1rhm  34199  mplidom  34202  extvfvcl  34210  esplyfval0  34238  esplyfval2  34239  esplyind  34249  vieta  34254  sradrng  34256  rlmdim  34284  ply1degltdimlem  34296  dimkerim  34301  lvecendof1f1o  34307  irngval  34359  extdgfialglem1  34366  minplym1p  34387  minplynzm1p  34388  algextdeglem3  34393  algextdeglem4  34394  algextdeglem5  34395  dispcmp  34533  ordtprsval  34592  ordtprsuni  34593  sitgval  35006  sseqval  35062  reprsuc  35286  lpadval  35350  bnj941  35445  bnj944  35610  subfacp1lem5  35991  sconnpht  36036  sconnpht2  36045  sconnpi1  36046  cvmliftlem7  36098  cvmliftlem10  36101  cvmlift2lem13  36122  cvmlift3lem9  36134  satffunlem1lem1  36209  satffunlem2lem1  36211  msrval  36345  mthmpps  36389  onint1  37279  bj-projeq  37947  bj-restsn  38045  finixpnum  38571  ptrest  38580  poimirlem4  38585  poimirlem13  38594  poimirlem14  38595  poimirlem16  38597  poimirlem19  38600  poimirlem26  38607  grpokerinj  38870  isdivrngo  38927  drngoi  38928  isprrngo  39027  lsatset  40090  lsmsat  40108  islshpat  40117  lflsc0N  40183  lkrfval  40187  ldualset  40225  dvafset  42104  dvaset  42105  dvhfset  42180  dvhset  42181  dibffval  42240  dibfval  42241  dib0  42264  cdlemn4a  42299  dihmeetlem4preN  42406  dihmeetlem13N  42419  dih1dimatlem  42429  dihlsprn  42431  dvh2dim  42545  lpolsetN  42582  lclkrlem2j  42616  lclkrlem2p  42622  lcfrlem21  42663  mapdpglem22  42793  mapdpglem23  42794  mapdpglem26  42798  mapdpglem27  42799  mapdpg  42806  baerlem3lem2  42810  baerlem5alem2  42811  baerlem5blem2  42812  baerlem5amN  42816  baerlem5bmN  42817  baerlem5abmN  42818  mapdindp4  42823  mapdhval  42824  mapdheq  42828  mapdh6aN  42835  hvmapffval  42858  hvmapfval  42859  hvmap1o2  42865  hdmap1fval  42896  hdmap1vallem  42897  hdmap1val  42898  hdmap1eq  42901  hdmap1cbv  42902  hdmap1l6a  42909  hdmapfval  42927  hdmap10  42940  hdmaprnlem6N  42954  hgmaprnlem2N  42997  lcmfunnnd  43105  aks6d1c6lem5  43270  qsalrel  43335  frlmsnic  43647  prjspval  43674  prjspval2  43684  prjspnvs  43691  prjcrvfval  43710  dfac11  44107  dfac21  44111  nzprmdif  45346  expgrowth  45362  fzdifsuc2  46369  cnrefiisplem  46882  cnrefiisp  46883  hoidmv1le  47647  ovnovollem3  47711  fsetsniunop  48162  fsetsnf  48164  fsetsnf1  48165  fsetsnfo  48166  dfateq12d  48239  otiunsndisjX  48392  funop1  48396  preimafvelsetpreimafv  48513  imaelsetpreimafv  48520  imasetpreimafvbijlemfo  48530  fundcmpsurbijinjpreimafv  48532  fundcmpsurinj  48534  fundcmpsurbijinj  48535  isprmrng  49476  lmod1zr  49648  0aryfvalel  49789  1arymaptf1  49797  discsubc  50215  imasubclem3  50257  swapf1a  50420  swapf2a  50422  swapf1  50423  swapf2  50425  termcbas2  50633  termchom  50639  termchom2  50640  termcfuncval  50683  mndtcval  50730