MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sneqd Structured version   Unicode version

Theorem sneqd 4026
Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)
Hypothesis
Ref Expression
sneqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
sneqd  |-  ( ph  ->  { A }  =  { B } )

Proof of Theorem sneqd
StepHypRef Expression
1 sneqd.1 . 2  |-  ( ph  ->  A  =  B )
2 sneq 4024 . 2  |-  ( A  =  B  ->  { A }  =  { B } )
31, 2syl 16 1  |-  ( ph  ->  { A }  =  { B } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   {csn 4014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-sn 4015
This theorem is referenced by:  otsndisj  4742  otiunsndisj  4743  dmsnopss  5470  dmsnsnsn  5476  cnvsng  5484  opswap  5485  ressn  5533  f1osng  5844  fsng  6055  fnressn  6068  fvsng  6090  2nd1st  6830  dfmpt2  6875  cnvf1olem  6883  suppsnop  6917  tpostpos  6977  tfrlem11  7059  ralxpmap  7470  elixpsn  7510  ixpsnf1o  7511  en1b  7585  mapsnen  7595  xpassen  7613  cantnfp1lem3  8102  cantnfp1lem3OLD  8128  wemapweOLD  8143  oef1oOLD  8145  axdc4lem  8838  ttukeylem3  8894  ttukey2g  8899  fpwwe2lem13  9023  fztp  11746  fzsuc2  11747  fseq1p1m1  11762  fseq1m1p1  11763  expval  12149  s1val  12591  s1eq  12593  fsumm1  13547  fprodm1  13752  divalgmod  14045  vdwpc  14479  vdwlem1  14480  vdwlem6  14485  vdwlem7  14486  vdwlem8  14487  cshwsdisj  14564  setsvalg  14636  strle1  14709  imasval  14889  imasaddvallem  14907  imasvscaval  14916  ismri2dad  15015  mreexd  15020  mreexmrid  15021  homaval  15336  setcmon  15392  gsumress  15881  pwsco2mhm  15980  mulgval  16122  symgval  16382  idressubgsymg  16413  gsumzsubmclOLD  16907  gsumzaddlem  16912  gsumzaddlemOLD  16914  pwsgsumOLD  16988  dmdprd  17007  dprdvalOLD  17014  subgdmdprd  17059  dprdsn  17061  dprd2da  17069  dmdprdpr  17076  dprdpr  17077  dpjfval  17082  dpjval  17083  ablfac1eulem  17101  pgpfaclem1  17110  isunit  17284  isdrng  17378  drngprop  17385  isdrngd  17399  drngpropd  17401  issubdrg  17432  lspsnneg  17630  lspsnsub  17631  lmodindp1  17638  islbs  17700  lspsntrim  17722  lbspropd  17723  lspsnvs  17738  lspsneleq  17739  lspfixed  17752  lpival  17871  psrval  17989  zrhrhmb  18525  znval  18549  isobs  18728  frlmval  18756  frlmgsumOLD  18778  frlmlbs  18808  islindf  18824  lindfmm  18839  lsslindf  18842  islindf4  18850  islindf5  18851  mat1dimmul  18955  mat1dimcrng  18956  mat1rhmval  18958  mat1ric  18966  mat1scmat  19018  mdet0pr  19071  m1detdiag  19076  pmatcoe1fsupp  19179  ordtval  19667  ordtcnv  19679  dissnlocfin  20007  ptval2  20079  dfac14  20096  txdis  20110  xkoptsub  20132  pt1hmeo  20284  xpstopnlem1  20287  xpstopnlem2  20289  tgptsmscls  20629  ustuqtoplem  20719  utopsnneiplem  20727  utopsnneip  20728  utop2nei  20730  utop3cls  20731  pcorev2  21505  pcophtb  21506  pi1grplem  21526  pi1inv  21529  cvsunit  21585  i1f1  22074  i1faddlem  22077  i1fmullem  22078  i1fadd  22079  limcfval  22253  dvnfval  22302  ig1pval  22550  0dgrb  22620  dgreq0  22638  dgrmulc  22644  plyrem  22677  facth  22678  fta1  22680  aaliou2  22712  taylpfval  22736  axlowdimlem15  24235  axlowdim  24240  1pthoncl  24570  2pthlem2  24574  eupath2lem3  24955  frgrancvvdeqlem4  25009  frgrancvvdeqlem6  25011  drngoi  25385  isdivrngo  25409  0ofval  25678  fcnvgreu  27490  dispcmp  27839  ordtprsval  27877  ordtprsuni  27878  indval2  28005  sitgval  28251  sseqval  28304  subfacp1lem5  28605  sconpht  28651  sconpht2  28660  sconpi1  28661  cvmliftlem7  28713  cvmliftlem10  28716  cvmlift2lem13  28737  cvmlift3lem9  28749  msrval  28875  mthmpps  28919  onint1  29889  finixpnum  30013  ptrest  30023  grpokerinj  30322  isprrngo  30422  dfac11  30983  dfac21  30987  dgrnznn  31060  nzprmdif  31200  expgrowth  31216  dfateq12d  32052  otiunsndisjX  32139  setsidvald  32392  lmod1zr  32829  bnj941  33564  bnj944  33729  bj-projeq  34298  lsatset  34455  lsmsat  34473  islshpat  34482  lflsc0N  34548  lkrfval  34552  ldualset  34590  dvafset  36470  dvaset  36471  dvhfset  36547  dvhset  36548  dibffval  36607  dibfval  36608  dib0  36631  cdlemn4a  36666  dihmeetlem4preN  36773  dihmeetlem13N  36786  dih1dimatlem  36796  dihlsprn  36798  dvh2dim  36912  lpolsetN  36949  lclkrlem2j  36983  lclkrlem2p  36989  lcfrlem21  37030  mapdpglem22  37160  mapdpglem23  37161  mapdpglem26  37165  mapdpglem27  37166  mapdpg  37173  baerlem3lem2  37177  baerlem5alem2  37178  baerlem5blem2  37179  baerlem5amN  37183  baerlem5bmN  37184  baerlem5abmN  37185  mapdindp4  37190  mapdhval  37191  mapdheq  37195  mapdh6aN  37202  hvmapffval  37225  hvmapfval  37226  hvmap1o2  37232  hdmap1fval  37264  hdmap1vallem  37265  hdmap1val  37266  hdmap1eq  37269  hdmap1cbv  37270  hdmap1l6a  37277  hdmap1neglem1N  37295  hdmapfval  37297  hdmap10  37310  hdmaprnlem6N  37324  hgmaprnlem2N  37367
  Copyright terms: Public domain W3C validator