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

Theorem dmeqd 5195
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 5193 . 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 1383   dom cdm 4989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-dm 4999
This theorem is referenced by:  dmxpid  5212  rneq  5218  dmxpss  5428  dmsnopss  5470  dmsnsnsn  5476  fndmin  5979  fninfp  6083  fndifnfp  6085  ovmpt3rabdm  6520  elxp4  6729  1stval  6787  fo1st  6805  f1stres  6807  bropopvvv  6865  suppsnop  6917  mpt2curryd  7000  errn  7335  xpassen  7613  xpdom2  7614  oicl  7957  oif  7958  hartogslem1  7970  cantnfdm  8084  cantnfdmOLD  8086  cantnfval  8090  cantnf0  8097  cantnfres  8099  cantnfvalOLD  8120  cnfcomlem  8146  cnfcomlemOLD  8154  hsmexlem4  8812  hsmexlem5  8813  axdc3lem2  8834  ttukeylem3  8894  hashfun  12476  swrdval  12625  s4dom  12848  shftdm  12885  rlim  13299  ramval  14507  isstruct2  14622  setsvalg  14636  prdsval  14833  homfeqbas  15072  invf  15143  oppciso  15152  sscfn1  15167  sscfn2  15168  isssc  15170  rescval  15177  rescval2  15178  issubc  15185  issubc2  15186  cofuval  15229  resfval  15239  resfval2  15240  resf1st  15241  prfval  15446  lubdm  15587  glbdm  15600  joindm  15611  meetdm  15625  islat  15655  isclat  15717  oduclatb  15752  gsumvalx  15875  cntzrcl  16343  f1omvdco2  16451  pmtrfrn  16461  symgsssg  16470  symgfisg  16471  symggen  16473  pmtrdifwrdellem3  16486  pmtrdifwrdel2lem1  16487  pmtrdifwrdel  16488  pmtrdifwrdel2  16489  psgnunilem1  16496  psgnunilem5  16497  psgnunilem2  16498  psgnunilem3  16499  psgneldm  16506  dmdprd  17007  dprdval  17012  dprdvalOLD  17014  dpjfval  17082  ablfaclem3  17116  mpfrcl  18165  zrhcofipsgn  18606  elocv  18676  ishil  18726  dsmmval  18742  mamudm  18867  mavmuldm  19029  mavmul0g  19032  m1detdiag  19076  decpmatval0  19242  decpmatval  19243  pmatcollpw3lem  19261  iscnp2  19717  ptval  20048  ptcmplem2  20530  cnextfval  20539  tsmsval2  20605  ustbas2  20705  utopval  20712  tusval  20746  ucnval  20757  iscfilu  20768  psmetdmdm  20786  xmetdmdm  20815  blfvalps  20863  setsmstopn  20958  tmsval  20961  metuvalOLD  21029  metuval  21030  tngtopn  21141  cfilfval  21680  caufval  21691  limcfval  22253  dvfval  22278  dvbsss  22283  perfdvf  22284  dvn2bss  22310  dvnres  22311  dvcmul  22324  dvcmulf  22325  dvcj  22330  dvnfre  22332  dvexp  22333  dvmptres3  22336  dvmptcl  22339  dvmptadd  22340  dvmptmul  22341  dvmptres2  22342  dvmptcmul  22344  dvmptcj  22348  dvmptco  22352  rolle  22368  cmvth  22369  mvth  22370  dvlip  22371  dvlipcn  22372  dvlip2  22373  c1liplem1  22374  dveq0  22378  dv11cn  22379  dvle  22385  dvivthlem1  22386  dvivth  22388  dvne0  22389  lhop1lem  22391  lhop2  22393  lhop  22394  dvcnvrelem1  22395  dvcvx  22398  dvfsumle  22399  dvfsumge  22400  dvfsumabs  22401  dvmptrecl  22402  dvfsumlem2  22405  itgsubstlem  22426  taylfval  22730  tayl0  22733  dvtaylp  22741  dvntaylp  22742  dvntaylp0  22743  taylthlem1  22744  taylthlem2  22745  ulmdvlem1  22771  pserdv  22800  pige3  22886  logtayl  23017  perpln1  24063  isushgra  24277  isumgra  24291  clwwlknprop  24748  2wlkonot3v  24851  2spthonot3v  24852  vdgrfval  24871  iseupa  24941  grporndm  25188  isabloda  25277  isass  25294  isexid  25295  ismndo2  25323  rngodm1dm2  25396  vcoprne  25448  hmoval  25701  metidval  27846  pstmval  27851  prsssdm  27876  ordtrestNEW  27880  ofcfval  28074  ofcfval3  28078  brae  28190  braew  28191  faeval  28195  mbfmcst  28207  issibf  28252  sitmval  28267  0rrv  28367  dstrvprob  28387  lgamgulmlem2  28549  relexpdm  29035  sdclem2  30210  ismtyval  30271  exidreslem  30314  divrngcl  30335  isdrngo2  30336  dvsconst  31211  expgrowth  31216  dvsinax  31612  dvmptresicc  31620  dvcosax  31627  dvbdfbdioolem1  31629  itgsinexplem1  31642  itgcoscmulx  31658  dirkeritg  31773  dirkercncflem2  31775  fourierdlem60  31838  fourierdlem61  31839  fourierdlem74  31852  fourierdlem75  31853  fourierdlem80  31858  fourierdlem94  31872  fourierdlem103  31881  fourierdlem104  31882  fourierdlem113  31891  dfateq12d  32052  isuhgr  32204  isushgr  32205  uhgeq12g  32208  uhguhgra  32210  uhgrauhg  32211  uhgrepe  32216  gsizval  32227  gsizopval  32229  estrreslem2  32493  mndpsuppss  32699  bj-finsumval0  34403  isopos  34645  isatl  34764  dibffval  36607  dibfval  36608  conrel2d  37465
  Copyright terms: Public domain W3C validator