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

Theorem dmeqd 5029
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 5027 . 2  |-  ( A  =  B  ->  dom  A  =  dom  B )
31, 2syl 16 1  |-  ( ph  ->  dom  A  =  dom  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362   dom cdm 4827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-dm 4837
This theorem is referenced by:  dmxpid  5046  rneq  5052  dmxpss  5257  dmsnopss  5299  dmsnsnsn  5305  fndmin  5798  fninfp  5892  fndifnfp  5894  elxp4  6511  1stval  6568  fo1st  6585  f1stres  6587  bropopvvv  6642  suppsnop  6693  errn  7111  xpassen  7393  xpdom2  7394  oicl  7731  oif  7732  hartogslem1  7744  cantnfdm  7858  cantnfdmOLD  7860  cantnfval  7864  cantnf0  7871  cantnfres  7873  cantnfvalOLD  7894  cnfcomlem  7920  cnfcomlemOLD  7928  hsmexlem4  8586  hsmexlem5  8587  axdc3lem2  8608  ttukeylem3  8668  hashfun  12182  swrdval  12296  s4dom  12512  shftdm  12543  rlim  12956  ramval  14051  isstruct2  14165  setsvalg  14179  prdsval  14375  homfeqbas  14617  invf  14688  oppciso  14697  sscfn1  14712  sscfn2  14713  isssc  14715  rescval  14722  rescval2  14723  issubc  14730  issubc2  14731  cofuval  14774  resfval  14784  resfval2  14785  resf1st  14786  prfval  14991  lubdm  15131  glbdm  15144  joindm  15155  meetdm  15169  islat  15199  isclat  15261  oduclatb  15296  gsumvalx  15483  cntzrcl  15824  f1omvdco2  15933  pmtrfrn  15943  symgsssg  15952  symgfisg  15953  symggen  15955  pmtrdifwrdellem3  15968  pmtrdifwrdel2lem1  15969  pmtrdifwrdel  15970  pmtrdifwrdel2  15971  psgnunilem1  15978  psgnunilem5  15979  psgnunilem2  15980  psgnunilem3  15981  psgneldm  15988  dmdprd  16453  dprdval  16458  dprdvalOLD  16460  dpjfval  16527  ablfaclem3  16561  zrhcofipsgn  17864  elocv  17934  ishil  17984  dsmmval  18000  mamudm  18129  mavmuldm  18202  mavmul0g  18205  iscnp2  18684  ptval  18984  ptcmplem2  19466  cnextfval  19475  tsmsval2  19541  ustbas2  19641  utopval  19648  tusval  19682  ucnval  19693  iscfilu  19704  psmetdmdm  19722  xmetdmdm  19751  blfvalps  19799  setsmstopn  19894  tmsval  19897  metuvalOLD  19965  metuval  19966  tngtopn  20077  cfilfval  20616  caufval  20627  limcfval  21188  dvfval  21213  dvbsss  21218  perfdvf  21219  dvn2bss  21245  dvnres  21246  dvcmul  21259  dvcmulf  21260  dvcj  21265  dvnfre  21267  dvexp  21268  dvmptres3  21271  dvmptcl  21274  dvmptadd  21275  dvmptmul  21276  dvmptres2  21277  dvmptcmul  21279  dvmptcj  21283  dvmptco  21287  rolle  21303  cmvth  21304  mvth  21305  dvlip  21306  dvlipcn  21307  dvlip2  21308  c1liplem1  21309  dveq0  21313  dv11cn  21314  dvle  21320  dvivthlem1  21321  dvivth  21323  dvne0  21324  lhop1lem  21326  lhop2  21328  lhop  21329  dvcnvrelem1  21330  dvcvx  21333  dvfsumle  21334  dvfsumge  21335  dvfsumabs  21336  dvmptrecl  21337  dvfsumlem2  21340  itgsubstlem  21361  mpfrcl  21369  taylfval  21708  tayl0  21711  dvtaylp  21719  dvntaylp  21720  dvntaylp0  21721  taylthlem1  21722  taylthlem2  21723  ulmdvlem1  21749  pserdv  21778  pige3  21863  logtayl  21989  isumgra  23071  vdgrfval  23387  iseupa  23408  grporndm  23519  isabloda  23608  isass  23625  isexid  23626  ismndo2  23654  rngodm1dm2  23727  vcoprne  23779  hmoval  24032  metidval  26170  pstmval  26175  prsssdm  26200  ordtrestNEW  26204  ofcfval  26393  ofcfval3  26397  brae  26510  braew  26511  faeval  26515  mbfmcst  26527  issibf  26566  sitmval  26581  0rrv  26681  dstrvprob  26701  lgamgulmlem2  26863  relexpdm  27183  sdclem2  28479  ismtyval  28540  exidreslem  28583  divrngcl  28604  isdrngo2  28605  dvsconst  29446  expgrowth  29451  itgsinexplem1  29637  dfateq12d  29878  ovmpt3rabdm  30005  2wlkonot3v  30237  2spthonot3v  30238  clwwlknprop  30278  mndpsuppss  30612  bj-finsumval0  32156  isopos  32395  isatl  32514  dibffval  34355  dibfval  34356
  Copyright terms: Public domain W3C validator