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

Theorem dmeqd 5205
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 5203 . 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 1379   dom cdm 4999
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-dm 5009
This theorem is referenced by:  dmxpid  5222  rneq  5228  dmxpss  5438  dmsnopss  5480  dmsnsnsn  5486  fndmin  5988  fninfp  6088  fndifnfp  6090  ovmpt3rabdm  6519  elxp4  6728  1stval  6786  fo1st  6804  f1stres  6806  bropopvvv  6863  suppsnop  6915  mpt2curryd  6998  errn  7333  xpassen  7611  xpdom2  7612  oicl  7954  oif  7955  hartogslem1  7967  cantnfdm  8081  cantnfdmOLD  8083  cantnfval  8087  cantnf0  8094  cantnfres  8096  cantnfvalOLD  8117  cnfcomlem  8143  cnfcomlemOLD  8151  hsmexlem4  8809  hsmexlem5  8810  axdc3lem2  8831  ttukeylem3  8891  hashfun  12461  swrdval  12607  s4dom  12830  shftdm  12867  rlim  13281  ramval  14385  isstruct2  14499  setsvalg  14513  prdsval  14710  homfeqbas  14952  invf  15023  oppciso  15032  sscfn1  15047  sscfn2  15048  isssc  15050  rescval  15057  rescval2  15058  issubc  15065  issubc2  15066  cofuval  15109  resfval  15119  resfval2  15120  resf1st  15121  prfval  15326  lubdm  15466  glbdm  15479  joindm  15490  meetdm  15504  islat  15534  isclat  15596  oduclatb  15631  gsumvalx  15824  cntzrcl  16170  f1omvdco2  16279  pmtrfrn  16289  symgsssg  16298  symgfisg  16299  symggen  16301  pmtrdifwrdellem3  16314  pmtrdifwrdel2lem1  16315  pmtrdifwrdel  16316  pmtrdifwrdel2  16317  psgnunilem1  16324  psgnunilem5  16325  psgnunilem2  16326  psgnunilem3  16327  psgneldm  16334  dmdprd  16832  dprdval  16837  dprdvalOLD  16839  dpjfval  16906  ablfaclem3  16940  mpfrcl  17986  zrhcofipsgn  18424  elocv  18494  ishil  18544  dsmmval  18560  mamudm  18685  mavmuldm  18847  mavmul0g  18850  m1detdiag  18894  decpmatval0  19060  decpmatval  19061  pmatcollpw3lem  19079  iscnp2  19534  ptval  19834  ptcmplem2  20316  cnextfval  20325  tsmsval2  20391  ustbas2  20491  utopval  20498  tusval  20532  ucnval  20543  iscfilu  20554  psmetdmdm  20572  xmetdmdm  20601  blfvalps  20649  setsmstopn  20744  tmsval  20747  metuvalOLD  20815  metuval  20816  tngtopn  20927  cfilfval  21466  caufval  21477  limcfval  22039  dvfval  22064  dvbsss  22069  perfdvf  22070  dvn2bss  22096  dvnres  22097  dvcmul  22110  dvcmulf  22111  dvcj  22116  dvnfre  22118  dvexp  22119  dvmptres3  22122  dvmptcl  22125  dvmptadd  22126  dvmptmul  22127  dvmptres2  22128  dvmptcmul  22130  dvmptcj  22134  dvmptco  22138  rolle  22154  cmvth  22155  mvth  22156  dvlip  22157  dvlipcn  22158  dvlip2  22159  c1liplem1  22160  dveq0  22164  dv11cn  22165  dvle  22171  dvivthlem1  22172  dvivth  22174  dvne0  22175  lhop1lem  22177  lhop2  22179  lhop  22180  dvcnvrelem1  22181  dvcvx  22184  dvfsumle  22185  dvfsumge  22186  dvfsumabs  22187  dvmptrecl  22188  dvfsumlem2  22191  itgsubstlem  22212  taylfval  22516  tayl0  22519  dvtaylp  22527  dvntaylp  22528  dvntaylp0  22529  taylthlem1  22530  taylthlem2  22531  ulmdvlem1  22557  pserdv  22586  pige3  22671  logtayl  22797  perpln1  23823  isushgra  24005  isumgra  24019  clwwlknprop  24476  2wlkonot3v  24579  2spthonot3v  24580  vdgrfval  24599  iseupa  24669  grporndm  24916  isabloda  25005  isass  25022  isexid  25023  ismndo2  25051  rngodm1dm2  25124  vcoprne  25176  hmoval  25429  metidval  27533  pstmval  27538  prsssdm  27563  ordtrestNEW  27567  ofcfval  27765  ofcfval3  27769  brae  27881  braew  27882  faeval  27886  mbfmcst  27898  issibf  27943  sitmval  27958  0rrv  28058  dstrvprob  28078  lgamgulmlem2  28240  relexpdm  28561  sdclem2  29866  ismtyval  29927  exidreslem  29970  divrngcl  29991  isdrngo2  29992  dvsconst  30863  expgrowth  30868  dvsinax  31269  dvmptresicc  31277  dvcosax  31284  dvbdfbdioolem1  31286  itgsinexplem1  31299  itgcoscmulx  31315  dirkeritg  31430  dirkercncflem2  31432  fourierdlem60  31495  fourierdlem61  31496  fourierdlem74  31509  fourierdlem75  31510  fourierdlem80  31515  fourierdlem94  31529  fourierdlem103  31538  fourierdlem104  31539  fourierdlem113  31548  dfateq12d  31709  isuhgr  31861  isushgr  31862  uhgeq12g  31865  uhguhgra  31867  uhgrauhg  31868  uhgrepe  31873  gsizval  31884  gsizopval  31886  mndpsuppss  32063  bj-finsumval0  33753  isopos  33995  isatl  34114  dibffval  35955  dibfval  35956  conrel2d  36800
  Copyright terms: Public domain W3C validator