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

Theorem dmeqd 5210
Description: Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
Hypothesis
Ref Expression
dmeqd.1
Assertion
Ref Expression
dmeqd

Proof of Theorem dmeqd
StepHypRef Expression
1 dmeqd.1 . 2
2 dmeq 5208 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  domcdm 5004
This theorem is referenced by:  dmxpid  5227  rneq  5233  dmxpss  5443  dmsnopss  5485  dmsnsnsn  5491  fndmin  5994  fninfp  6098  fndifnfp  6100  ovmpt3rabdm  6535  elxp4  6744  1stval  6802  fo1st  6820  f1stres  6822  bropopvvv  6880  suppsnop  6932  mpt2curryd  7017  errn  7352  xpassen  7631  xpdom2  7632  oicl  7975  oif  7976  hartogslem1  7988  cantnfdm  8102  cantnfdmOLD  8104  cantnfval  8108  cantnf0  8115  cantnfres  8117  cantnfvalOLD  8138  cnfcomlem  8164  cnfcomlemOLD  8172  hsmexlem4  8830  hsmexlem5  8831  axdc3lem2  8852  ttukeylem3  8912  hashfun  12495  swrdval  12644  s4dom  12867  shftdm  12904  rlim  13318  ramval  14526  isstruct2  14641  setsvalg  14655  prdsval  14852  homfeqbas  15091  invf  15162  oppciso  15171  sscfn1  15186  sscfn2  15187  isssc  15189  rescval  15196  rescval2  15197  issubc  15204  issubc2  15205  cofuval  15251  resfval  15261  resfval2  15262  resf1st  15263  prfval  15468  lubdm  15609  glbdm  15622  joindm  15633  meetdm  15647  islat  15677  isclat  15739  oduclatb  15774  gsumvalx  15897  cntzrcl  16365  f1omvdco2  16473  pmtrfrn  16483  symgsssg  16492  symgfisg  16493  symggen  16495  pmtrdifwrdellem3  16508  pmtrdifwrdel2lem1  16509  pmtrdifwrdel  16510  pmtrdifwrdel2  16511  psgnunilem1  16518  psgnunilem5  16519  psgnunilem2  16520  psgnunilem3  16521  psgneldm  16528  dmdprd  17029  dprdval  17034  dprdvalOLD  17036  dpjfval  17104  ablfaclem3  17138  mpfrcl  18187  zrhcofipsgn  18629  elocv  18699  ishil  18749  dsmmval  18765  mamudm  18890  mavmuldm  19052  mavmul0g  19055  m1detdiag  19099  decpmatval0  19265  decpmatval  19266  pmatcollpw3lem  19284  iscnp2  19740  ptval  20071  ptcmplem2  20553  cnextfval  20562  tsmsval2  20628  ustbas2  20728  utopval  20735  tusval  20769  ucnval  20780  iscfilu  20791  psmetdmdm  20809  xmetdmdm  20838  blfvalps  20886  setsmstopn  20981  tmsval  20984  metuvalOLD  21052  metuval  21053  tngtopn  21164  cfilfval  21703  caufval  21714  limcfval  22276  dvfval  22301  dvbsss  22306  perfdvf  22307  dvn2bss  22333  dvnres  22334  dvcmul  22347  dvcmulf  22348  dvcj  22353  dvnfre  22355  dvexp  22356  dvmptres3  22359  dvmptcl  22362  dvmptadd  22363  dvmptmul  22364  dvmptres2  22365  dvmptcmul  22367  dvmptcj  22371  dvmptco  22375  rolle  22391  cmvth  22392  mvth  22393  dvlip  22394  dvlipcn  22395  dvlip2  22396  c1liplem1  22397  dveq0  22401  dv11cn  22402  dvle  22408  dvivthlem1  22409  dvivth  22411  dvne0  22412  lhop1lem  22414  lhop2  22416  lhop  22417  dvcnvrelem1  22418  dvcvx  22421  dvfsumle  22422  dvfsumge  22423  dvfsumabs  22424  dvmptrecl  22425  dvfsumlem2  22428  itgsubstlem  22449  taylfval  22754  tayl0  22757  dvtaylp  22765  dvntaylp  22766  dvntaylp0  22767  taylthlem1  22768  taylthlem2  22769  ulmdvlem1  22795  pserdv  22824  pige3  22910  logtayl  23041  perpln1  24087  isushgra  24301  isumgra  24315  clwwlknprop  24772  2wlkonot3v  24875  2spthonot3v  24876  vdgrfval  24895  iseupa  24965  grporndm  25212  isabloda  25301  isass  25318  isexid  25319  ismndo2  25347  rngodm1dm2  25420  vcoprne  25472  hmoval  25725  metidval  27869  pstmval  27874  prsssdm  27899  ordtrestNEW  27903  ofcfval  28097  ofcfval3  28101  brae  28213  braew  28214  faeval  28218  mbfmcst  28230  issibf  28275  sitmval  28290  0rrv  28390  dstrvprob  28410  lgamgulmlem2  28572  relexpdm  29058  sdclem2  30235  ismtyval  30296  exidreslem  30339  divrngcl  30360  isdrngo2  30361  dvsconst  31235  expgrowth  31240  dvsinax  31708  dvmptresicc  31716  dvcosax  31723  dvbdfbdioolem1  31725  itgsinexplem1  31752  itgcoscmulx  31768  dirkeritg  31884  dirkercncflem2  31886  fourierdlem60  31949  fourierdlem61  31950  fourierdlem74  31963  fourierdlem75  31964  fourierdlem80  31969  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  fourierdlem113  32002  dfateq12d  32214  isuhgr  32366  isushgr  32367  uhgeq12g  32370  uhguhgra  32372  uhgrauhg  32373  uhgrepe  32378  gsizval  32389  gsizopval  32391  dfiso2  32568  cicsym  32588  estrreslem2  32644  mndpsuppss  32964  bj-finsumval0  34663  isopos  34905  isatl  35024  dibffval  36867  dibfval  36868  conrel2d  37762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-dm 5014
  Copyright terms: Public domain W3C validator