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

Theorem dmeqd 4897
Description: Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)
Hypothesis
Ref Expression
dmeqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
dmeqd  |-  ( ph  ->  dom  A  =  dom  B )

Proof of Theorem dmeqd
StepHypRef Expression
1 dmeqd.1 . 2  |-  ( ph  ->  A  =  B )
2 dmeq 4895 . 2  |-  ( A  =  B  ->  dom  A  =  dom  B )
31, 2syl 15 1  |-  ( ph  ->  dom  A  =  dom  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   dom cdm 4705
This theorem is referenced by:  dmxpid  4914  rneq  4920  dmxpss  5123  dmsnopss  5161  dmsnsnsn  5167  elxp4  5176  fndmin  5648  1stval  6140  fo1st  6155  f1stres  6157  errn  6698  xpassen  6972  xpdom2  6973  oicl  7260  oif  7261  hartogslem1  7273  cantnfdm  7381  cantnfval  7385  cantnf0  7392  cantnfres  7395  cnfcomlem  7418  hsmexlem4  8071  hsmexlem5  8072  axdc3lem2  8093  ttukeylem3  8154  hashfun  11405  swrdval  11466  shftdm  11582  rlim  11985  ramval  13071  isstruct2  13173  setsvalg  13187  prdsval  13371  homfeqbas  13615  invf  13686  oppciso  13695  sscfn1  13710  sscfn2  13711  isssc  13713  rescval  13720  rescval2  13721  issubc  13728  issubc2  13729  cofuval  13772  resfval  13782  resfval2  13783  resf1st  13784  prfval  13989  gsumvalx  14467  cntzrcl  14819  dmdprd  15252  dprdval  15254  dpjfval  15306  ablfaclem3  15338  elocv  16584  ishil  16634  iscnp2  16985  ptval  17281  ptcmplem2  17763  tsmsval2  17828  xmetdmdm  17916  blfval  17963  setsmstopn  18040  tmsval  18043  tngtopn  18182  cfilfval  18706  caufval  18717  limcfval  19238  dvfval  19263  dvbsss  19268  perfdvf  19269  dvn2bss  19295  dvnres  19296  dvcmul  19309  dvcmulf  19310  dvcj  19315  dvnfre  19317  dvexp  19318  dvmptres3  19321  dvmptcl  19324  dvmptadd  19325  dvmptmul  19326  dvmptres2  19327  dvmptcmul  19329  dvmptcj  19333  dvmptco  19337  rolle  19353  cmvth  19354  mvth  19355  dvlip  19356  dvlipcn  19357  dvlip2  19358  c1liplem1  19359  dveq0  19363  dv11cn  19364  dvle  19370  dvivthlem1  19371  dvivth  19373  dvne0  19374  lhop1lem  19376  lhop2  19378  lhop  19379  dvcnvrelem1  19380  dvcvx  19383  dvfsumle  19384  dvfsumge  19385  dvfsumabs  19386  dvmptrecl  19387  dvfsumlem2  19390  itgsubstlem  19411  mpfrcl  19418  taylfval  19754  tayl0  19757  dvtaylp  19765  dvntaylp  19766  dvntaylp0  19767  taylthlem1  19768  taylthlem2  19769  ulmdvlem1  19793  pserdv  19821  pige3  19901  logtayl  20023  grporndm  20893  isabloda  20982  isass  20999  isexid  21000  ismndo2  21028  rngodm1dm2  21101  vcoprne  21151  hmoval  21404  ofcfval  23474  ofcfval3  23478  mbfmcst  23579  isibfm  23608  0rrv  23669  dstrvprob  23687  isumgra  23882  iseupa  23896  vdgrfval  23904  relexpdm  24047  areacirclem3  25029  rnintintrn  25229  iscst1  25277  islatalg  25286  cur1val  25301  cur1vald  25302  iscom  25436  zintdom  25541  ishoma  25890  ishomd  25893  ismona  25912  isepia  25922  isiso  25928  cinvlem1  25931  isfuna  25937  isinob  25965  issrc  25970  propsrc  25971  isntr  25976  islimcat  25979  valdom  25987  prismorcsetlem  26015  prismorcset  26017  cmppar2  26075  bosser  26270  sdclem2  26555  ismtyval  26627  exidreslem  26670  divrngcl  26691  isdrngo2  26692  fninfp  26857  fndifnfp  26859  dsmmval  27303  f1omvdco2  27494  pmtrfrn  27503  symgsssg  27511  symgfisg  27512  symggen  27514  psgnunilem1  27519  psgnunilem5  27520  psgnunilem2  27521  psgnunilem3  27522  psgneldm  27529  dvsconst  27650  expgrowth  27655  itgsinexplem1  27851  dfateq12d  28097  s4dom  28224  trlonprop  28341  dibffval  31952  dibfval  31953
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-dm 4715
  Copyright terms: Public domain W3C validator