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

Theorem dmeqd 5063
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 5061 . 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 1369   dom cdm 4861
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314  df-dm 4871
This theorem is referenced by:  dmxpid  5080  rneq  5086  dmxpss  5290  dmsnopss  5332  dmsnsnsn  5338  fndmin  5831  fninfp  5926  fndifnfp  5928  elxp4  6543  1stval  6600  fo1st  6617  f1stres  6619  bropopvvv  6674  suppsnop  6725  mpt2curryd  6809  errn  7144  xpassen  7426  xpdom2  7427  oicl  7764  oif  7765  hartogslem1  7777  cantnfdm  7891  cantnfdmOLD  7893  cantnfval  7897  cantnf0  7904  cantnfres  7906  cantnfvalOLD  7927  cnfcomlem  7953  cnfcomlemOLD  7961  hsmexlem4  8619  hsmexlem5  8620  axdc3lem2  8641  ttukeylem3  8701  hashfun  12220  swrdval  12334  s4dom  12550  shftdm  12581  rlim  12994  ramval  14090  isstruct2  14204  setsvalg  14218  prdsval  14414  homfeqbas  14656  invf  14727  oppciso  14736  sscfn1  14751  sscfn2  14752  isssc  14754  rescval  14761  rescval2  14762  issubc  14769  issubc2  14770  cofuval  14813  resfval  14823  resfval2  14824  resf1st  14825  prfval  15030  lubdm  15170  glbdm  15183  joindm  15194  meetdm  15208  islat  15238  isclat  15300  oduclatb  15335  gsumvalx  15523  cntzrcl  15866  f1omvdco2  15975  pmtrfrn  15985  symgsssg  15994  symgfisg  15995  symggen  15997  pmtrdifwrdellem3  16010  pmtrdifwrdel2lem1  16011  pmtrdifwrdel  16012  pmtrdifwrdel2  16013  psgnunilem1  16020  psgnunilem5  16021  psgnunilem2  16022  psgnunilem3  16023  psgneldm  16030  dmdprd  16502  dprdval  16507  dprdvalOLD  16509  dpjfval  16576  ablfaclem3  16610  mpfrcl  17626  zrhcofipsgn  18045  elocv  18115  ishil  18165  dsmmval  18181  mamudm  18310  mavmuldm  18383  mavmul0g  18386  iscnp2  18865  ptval  19165  ptcmplem2  19647  cnextfval  19656  tsmsval2  19722  ustbas2  19822  utopval  19829  tusval  19863  ucnval  19874  iscfilu  19885  psmetdmdm  19903  xmetdmdm  19932  blfvalps  19980  setsmstopn  20075  tmsval  20078  metuvalOLD  20146  metuval  20147  tngtopn  20258  cfilfval  20797  caufval  20808  limcfval  21369  dvfval  21394  dvbsss  21399  perfdvf  21400  dvn2bss  21426  dvnres  21427  dvcmul  21440  dvcmulf  21441  dvcj  21446  dvnfre  21448  dvexp  21449  dvmptres3  21452  dvmptcl  21455  dvmptadd  21456  dvmptmul  21457  dvmptres2  21458  dvmptcmul  21460  dvmptcj  21464  dvmptco  21468  rolle  21484  cmvth  21485  mvth  21486  dvlip  21487  dvlipcn  21488  dvlip2  21489  c1liplem1  21490  dveq0  21494  dv11cn  21495  dvle  21501  dvivthlem1  21502  dvivth  21504  dvne0  21505  lhop1lem  21507  lhop2  21509  lhop  21510  dvcnvrelem1  21511  dvcvx  21514  dvfsumle  21515  dvfsumge  21516  dvfsumabs  21517  dvmptrecl  21518  dvfsumlem2  21521  itgsubstlem  21542  taylfval  21846  tayl0  21849  dvtaylp  21857  dvntaylp  21858  dvntaylp0  21859  taylthlem1  21860  taylthlem2  21861  ulmdvlem1  21887  pserdv  21916  pige3  22001  logtayl  22127  isumgra  23271  vdgrfval  23587  iseupa  23608  grporndm  23719  isabloda  23808  isass  23825  isexid  23826  ismndo2  23854  rngodm1dm2  23927  vcoprne  23979  hmoval  24232  metidval  26339  pstmval  26344  prsssdm  26369  ordtrestNEW  26373  ofcfval  26562  ofcfval3  26566  brae  26679  braew  26680  faeval  26684  mbfmcst  26696  issibf  26741  sitmval  26756  0rrv  26856  dstrvprob  26876  lgamgulmlem2  27038  relexpdm  27359  sdclem2  28664  ismtyval  28725  exidreslem  28768  divrngcl  28789  isdrngo2  28790  dvsconst  29630  expgrowth  29635  itgsinexplem1  29820  dfateq12d  30061  ovmpt3rabdm  30188  2wlkonot3v  30420  2spthonot3v  30421  clwwlknprop  30461  mndpsuppss  30814  m1detdiag  30931  bj-finsumval0  32679  isopos  32921  isatl  33040  dibffval  34881  dibfval  34882
  Copyright terms: Public domain W3C validator