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

Theorem dmeqd 4881
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 4879 . 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 1623   dom cdm 4689
This theorem is referenced by:  dmxpid  4898  rneq  4904  dmxpss  5107  dmsnopss  5145  dmsnsnsn  5151  elxp4  5160  fndmin  5632  1stval  6124  fo1st  6139  f1stres  6141  errn  6682  xpassen  6956  xpdom2  6957  oicl  7244  oif  7245  hartogslem1  7257  cantnfdm  7365  cantnfval  7369  cantnf0  7376  cantnfres  7379  cnfcomlem  7402  hsmexlem4  8055  hsmexlem5  8056  axdc3lem2  8077  ttukeylem3  8138  hashfun  11389  swrdval  11450  shftdm  11566  rlim  11969  ramval  13055  isstruct2  13157  setsvalg  13171  prdsval  13355  homfeqbas  13599  invf  13670  oppciso  13679  sscfn1  13694  sscfn2  13695  isssc  13697  rescval  13704  rescval2  13705  issubc  13712  issubc2  13713  cofuval  13756  resfval  13766  resfval2  13767  resf1st  13768  prfval  13973  gsumvalx  14451  cntzrcl  14803  dmdprd  15236  dprdval  15238  dpjfval  15290  ablfaclem3  15322  elocv  16568  ishil  16618  iscnp2  16969  ptval  17265  ptcmplem2  17747  tsmsval2  17812  xmetdmdm  17900  blfval  17947  setsmstopn  18024  tmsval  18027  tngtopn  18166  cfilfval  18690  caufval  18701  limcfval  19222  dvfval  19247  dvbsss  19252  perfdvf  19253  dvn2bss  19279  dvnres  19280  dvcmul  19293  dvcmulf  19294  dvcj  19299  dvnfre  19301  dvexp  19302  dvmptres3  19305  dvmptcl  19308  dvmptadd  19309  dvmptmul  19310  dvmptres2  19311  dvmptcmul  19313  dvmptcj  19317  dvmptco  19321  rolle  19337  cmvth  19338  mvth  19339  dvlip  19340  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  dveq0  19347  dv11cn  19348  dvle  19354  dvivthlem1  19355  dvivth  19357  dvne0  19358  lhop1lem  19360  lhop2  19362  lhop  19363  dvcnvrelem1  19364  dvcvx  19367  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvmptrecl  19371  dvfsumlem2  19374  itgsubstlem  19395  mpfrcl  19402  taylfval  19738  tayl0  19741  dvtaylp  19749  dvntaylp  19750  dvntaylp0  19751  taylthlem1  19752  taylthlem2  19753  ulmdvlem1  19777  pserdv  19805  pige3  19885  logtayl  20007  grporndm  20877  isabloda  20966  isass  20983  isexid  20984  ismndo2  21012  rngodm1dm2  21085  vcoprne  21135  hmoval  21388  ofcfval  23459  ofcfval3  23463  mbfmcst  23564  isibfm  23593  0rrv  23654  dstrvprob  23672  isumgra  23867  iseupa  23881  vdgrfval  23889  relexpdm  24032  areacirclem3  24926  rnintintrn  25126  iscst1  25174  islatalg  25183  cur1val  25198  cur1vald  25199  iscom  25333  zintdom  25438  ishoma  25787  ishomd  25790  ismona  25809  isepia  25819  isiso  25825  cinvlem1  25828  isfuna  25834  isinob  25862  issrc  25867  propsrc  25868  isntr  25873  islimcat  25876  valdom  25884  prismorcsetlem  25912  prismorcset  25914  cmppar2  25972  bosser  26167  sdclem2  26452  ismtyval  26524  exidreslem  26567  divrngcl  26588  isdrngo2  26589  fninfp  26754  fndifnfp  26756  dsmmval  27200  f1omvdco2  27391  pmtrfrn  27400  symgsssg  27408  symgfisg  27409  symggen  27411  psgnunilem1  27416  psgnunilem5  27417  psgnunilem2  27418  psgnunilem3  27419  psgneldm  27426  dvsconst  27547  expgrowth  27552  itgsinexplem1  27748  dfateq12d  27992  s4dom  28092  dibffval  31330  dibfval  31331
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-dm 4699
  Copyright terms: Public domain W3C validator