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

Theorem dmeqd 5059
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 5057 . 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 1455   dom cdm 4856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4419  df-dm 4866
This theorem is referenced by:  dmxpid  5076  rneq  5082  dmxpss  5290  dmsnopss  5331  dmsnsnsn  5337  f10d  5873  fndmin  6017  fninfp  6120  fndifnfp  6122  ovmpt3rabdm  6558  elxp4  6769  1stval  6827  fo1st  6845  f1stres  6847  bropopvvv  6906  bropfvvvv  6908  suppsnop  6960  mpt2curryd  7047  errn  7416  xpassen  7697  xpdom2  7698  oicl  8075  oif  8076  hartogslem1  8088  cantnfdm  8200  cantnfval  8204  cantnf0  8211  cantnfres  8213  cnfcomlem  8235  hsmexlem4  8890  hsmexlem5  8891  axdc3lem2  8912  ttukeylem3  8972  hashfun  12648  s1dmALT  12789  swrdval  12816  swrd0  12833  s2dmALT  13045  s4dom  13056  dmtrclfv  13137  relexpnndm  13159  relexpdmg  13160  relexpnnrn  13163  relexpfld  13167  relexpaddg  13171  shftdm  13189  rlim  13614  ramval  15015  ramvalOLD  15016  isstruct2  15185  setsvalg  15200  prdsval  15408  homfeqbas  15656  invf  15728  dfiso2  15732  oppciso  15741  cicsym  15764  sscfn1  15777  sscfn2  15778  isssc  15780  rescval  15787  rescval2  15788  issubc  15795  issubc2  15796  cofuval  15842  resfval  15852  resfval2  15853  resf1st  15854  estrreslem2  16078  prfval  16139  lubdm  16280  glbdm  16293  joindm  16304  meetdm  16318  islat  16348  isclat  16410  oduclatb  16445  gsumvalx  16568  cntzrcl  17036  f1omvdco2  17144  pmtrfrn  17154  symgsssg  17163  symgfisg  17164  symggen  17166  pmtrdifwrdellem3  17179  pmtrdifwrdel2lem1  17180  pmtrdifwrdel  17181  pmtrdifwrdel2  17182  psgnunilem1  17189  psgnunilem5  17190  psgnunilem2  17191  psgnunilem3  17192  psgneldm  17199  dmdprd  17685  dprdval  17690  dpjfval  17743  ablfaclem3  17775  mpfrcl  18796  zrhcofipsgn  19216  elocv  19286  ishil  19336  dsmmval  19352  mamudm  19468  mavmuldm  19630  mavmul0g  19633  m1detdiag  19677  decpmatval0  19843  decpmatval  19844  pmatcollpw3lem  19862  iscnp2  20310  ptval  20640  ptcmplem2  21123  cnextfval  21132  tsmsval2  21199  ustbas2  21295  utopval  21302  tusval  21336  ucnval  21347  iscfilu  21358  psmetdmdm  21376  xmetdmdm  21405  blfvalps  21453  setsmstopn  21548  tmsval  21551  metuval  21619  tngtopn  21713  cfilfval  22289  caufval  22300  limcfval  22883  dvfval  22908  dvbsss  22913  perfdvf  22914  dvn2bss  22940  dvnres  22941  dvcmul  22954  dvcmulf  22955  dvcj  22960  dvnfre  22962  dvexp  22963  dvmptres3  22966  dvmptcl  22969  dvmptadd  22970  dvmptmul  22971  dvmptres2  22972  dvmptcmul  22974  dvmptcj  22978  dvmptco  22982  rolle  22998  cmvth  22999  mvth  23000  dvlip  23001  dvlipcn  23002  dvlip2  23003  c1liplem1  23004  dveq0  23008  dv11cn  23009  dvle  23015  dvivthlem1  23016  dvivth  23018  dvne0  23019  lhop1lem  23021  lhop2  23023  lhop  23024  dvcnvrelem1  23025  dvcvx  23028  dvfsumle  23029  dvfsumge  23030  dvfsumabs  23031  dvmptrecl  23032  dvfsumlem2  23035  itgsubstlem  23056  taylfval  23370  tayl0  23373  dvtaylp  23381  dvntaylp  23382  dvntaylp0  23383  taylthlem1  23384  taylthlem2  23385  ulmdvlem1  23411  pserdv  23440  pige3  23528  logtayl  23661  relogbf  23784  lgamgulmlem2  24011  perpln1  24811  isushgra  25084  isumgra  25098  clwwlknprop  25556  2wlkonot3v  25659  2spthonot3v  25660  vdgrfval  25679  iseupa  25749  grporndm  25994  isabloda  26083  isass  26100  isexid  26101  ismndo2  26129  rngodm1dm2  26202  vcoprne  26254  hmoval  26507  smatrcl  28673  metidval  28744  pstmval  28749  prsssdm  28774  ordtrestNEW  28778  ofcfval  28970  ofcfval3  28974  brae  29114  braew  29115  faeval  29119  mbfmcst  29131  carsgval  29185  issibf  29216  sitmval  29232  0rrv  29334  dstrvprob  29354  bj-finsumval0  31748  sdclem2  32117  ismtyval  32178  exidreslem  32221  divrngcl  32242  isdrngo2  32243  isopos  32792  isatl  32911  dibffval  34754  dibfval  34755  conrel2d  36302  iunrelexp0  36340  dmtrclfvRP  36368  rntrclfvRP  36369  dvsconst  36724  expgrowth  36729  dvsinax  37869  dvmptresicc  37877  dvcosax  37884  dvbdfbdioolem1  37886  itgsinexplem1  37916  itgcoscmulx  37932  dirkeritg  38065  dirkercncflem2  38067  fourierdlem60  38131  fourierdlem61  38132  fourierdlem74  38145  fourierdlem75  38146  fourierdlem80  38151  fourierdlem94  38165  fourierdlem103  38174  fourierdlem104  38175  fourierdlem113  38184  dmvon  38535  ovnovollem1  38585  dfateq12d  38766  isuhgr  39293  isushgr  39294  uhgreq12g  39298  uhgruhgra  39303  uhgrauhgr  39304  isuhgrop  39306  uhgrun  39310  isupgr  39319  isumgr  39328  upgr1e  39345  upgrun  39350  umgrun  39352  isuspgr  39383  isusgr  39384  isusgrop  39393  ausgrusgrb  39396  uspgr1e  39465  usgrexmpl  39481  issubgr  39489  uhgrspansubgrlem  39508  usgrexi  39652  vtxdgfval  39674  vtxduhgrun  39684  umgr2v2e  39708  umgr2v2evd2  39710  ewlksfval  39764  1wlksfval  39770  wlksfval  39771  isuhgrALTV  40047  isushgrALTV  40048  uhgeq12gALTV  40051  uhguhgra  40053  uhgrauhg  40054  uhgrepe  40059  gsizval  40070  gsizopval  40072  mndpsuppss  40525
  Copyright terms: Public domain W3C validator