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

Theorem dmeqd 5056
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 5054 . 2  |-  ( A  =  B  ->  dom  A  =  dom  B )
31, 2syl 17 1  |-  ( ph  ->  dom  A  =  dom  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   dom cdm 4853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-dm 4863
This theorem is referenced by:  dmxpid  5073  rneq  5079  dmxpss  5287  dmsnopss  5327  dmsnsnsn  5333  fndmin  6004  fninfp  6106  fndifnfp  6108  ovmpt3rabdm  6540  elxp4  6751  1stval  6809  fo1st  6827  f1stres  6829  bropopvvv  6887  suppsnop  6939  mpt2curryd  7027  errn  7396  xpassen  7675  xpdom2  7676  oicl  8053  oif  8054  hartogslem1  8066  cantnfdm  8177  cantnfval  8181  cantnf0  8188  cantnfres  8190  cnfcomlem  8212  hsmexlem4  8866  hsmexlem5  8867  axdc3lem2  8888  ttukeylem3  8948  hashfun  12613  swrdval  12775  swrd0  12792  s4dom  13004  dmtrclfv  13082  relexpnndm  13104  relexpdmg  13105  relexpnnrn  13108  relexpfld  13112  relexpaddg  13116  shftdm  13134  rlim  13558  ramval  14959  ramvalOLD  14960  isstruct2  15129  setsvalg  15144  prdsval  15352  homfeqbas  15600  invf  15672  dfiso2  15676  oppciso  15685  cicsym  15708  sscfn1  15721  sscfn2  15722  isssc  15724  rescval  15731  rescval2  15732  issubc  15739  issubc2  15740  cofuval  15786  resfval  15796  resfval2  15797  resf1st  15798  estrreslem2  16022  prfval  16083  lubdm  16224  glbdm  16237  joindm  16248  meetdm  16262  islat  16292  isclat  16354  oduclatb  16389  gsumvalx  16512  cntzrcl  16980  f1omvdco2  17088  pmtrfrn  17098  symgsssg  17107  symgfisg  17108  symggen  17110  pmtrdifwrdellem3  17123  pmtrdifwrdel2lem1  17124  pmtrdifwrdel  17125  pmtrdifwrdel2  17126  psgnunilem1  17133  psgnunilem5  17134  psgnunilem2  17135  psgnunilem3  17136  psgneldm  17143  dmdprd  17629  dprdval  17634  dpjfval  17687  ablfaclem3  17719  mpfrcl  18740  zrhcofipsgn  19159  elocv  19229  ishil  19279  dsmmval  19295  mamudm  19411  mavmuldm  19573  mavmul0g  19576  m1detdiag  19620  decpmatval0  19786  decpmatval  19787  pmatcollpw3lem  19805  iscnp2  20253  ptval  20583  ptcmplem2  21066  cnextfval  21075  tsmsval2  21142  ustbas2  21238  utopval  21245  tusval  21279  ucnval  21290  iscfilu  21301  psmetdmdm  21319  xmetdmdm  21348  blfvalps  21396  setsmstopn  21491  tmsval  21494  metuval  21562  tngtopn  21656  cfilfval  22232  caufval  22243  limcfval  22825  dvfval  22850  dvbsss  22855  perfdvf  22856  dvn2bss  22882  dvnres  22883  dvcmul  22896  dvcmulf  22897  dvcj  22902  dvnfre  22904  dvexp  22905  dvmptres3  22908  dvmptcl  22911  dvmptadd  22912  dvmptmul  22913  dvmptres2  22914  dvmptcmul  22916  dvmptcj  22920  dvmptco  22924  rolle  22940  cmvth  22941  mvth  22942  dvlip  22943  dvlipcn  22944  dvlip2  22945  c1liplem1  22946  dveq0  22950  dv11cn  22951  dvle  22957  dvivthlem1  22958  dvivth  22960  dvne0  22961  lhop1lem  22963  lhop2  22965  lhop  22966  dvcnvrelem1  22967  dvcvx  22970  dvfsumle  22971  dvfsumge  22972  dvfsumabs  22973  dvmptrecl  22974  dvfsumlem2  22977  itgsubstlem  22998  taylfval  23312  tayl0  23315  dvtaylp  23323  dvntaylp  23324  dvntaylp0  23325  taylthlem1  23326  taylthlem2  23327  ulmdvlem1  23353  pserdv  23382  pige3  23470  logtayl  23603  relogbf  23726  lgamgulmlem2  23953  perpln1  24753  isushgra  25026  isumgra  25040  clwwlknprop  25498  2wlkonot3v  25601  2spthonot3v  25602  vdgrfval  25621  iseupa  25691  grporndm  25936  isabloda  26025  isass  26042  isexid  26043  ismndo2  26071  rngodm1dm2  26144  vcoprne  26196  hmoval  26449  smatrcl  28630  metidval  28701  pstmval  28706  prsssdm  28731  ordtrestNEW  28735  ofcfval  28927  ofcfval3  28931  brae  29072  braew  29073  faeval  29077  mbfmcst  29089  carsgval  29143  issibf  29174  sitmval  29190  0rrv  29292  dstrvprob  29312  bj-finsumval0  31666  sdclem2  32035  ismtyval  32096  exidreslem  32139  divrngcl  32160  isdrngo2  32161  isopos  32715  isatl  32834  dibffval  34677  dibfval  34678  conrel2d  36226  iunrelexp0  36264  dmtrclfvRP  36292  rntrclfvRP  36293  dvsconst  36649  expgrowth  36654  dvsinax  37723  dvmptresicc  37731  dvcosax  37738  dvbdfbdioolem1  37740  itgsinexplem1  37770  itgcoscmulx  37786  dirkeritg  37904  dirkercncflem2  37906  fourierdlem60  37970  fourierdlem61  37971  fourierdlem74  37984  fourierdlem75  37985  fourierdlem80  37990  fourierdlem94  38004  fourierdlem103  38013  fourierdlem104  38014  fourierdlem113  38023  dfateq12d  38501  isuhgr  38980  isushgr  38981  uhgreq12g  38987  uhgruhgra  38989  uhgrauhgr  38990  uhgrop  38992  uhgrun  38997  isumgr  39003  umgr0  39012  umgr1  39014  umgrun  39020  isuspgr  39032  isusgr  39033  ausgrusgrb  39046  usgr0e  39092  uspgr1  39099  usgrexmpl  39111  issubgr  39116  uhgrspansubgrlem  39133  usgrexi  39262  isuhgrALTV  39297  isushgrALTV  39298  uhgeq12gALTV  39301  uhguhgra  39303  uhgrauhg  39304  uhgrepe  39309  gsizval  39320  gsizopval  39322  mndpsuppss  39777
  Copyright terms: Public domain W3C validator