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

Theorem dmeqd 5031
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 5029 . 2  |-  ( A  =  B  ->  dom  A  =  dom  B )
31, 2syl 16 1  |-  ( ph  ->  dom  A  =  dom  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   dom cdm 4837
This theorem is referenced by:  dmxpid  5048  rneq  5054  dmxpss  5259  dmsnopss  5301  dmsnsnsn  5307  elxp4  5316  fndmin  5796  1stval  6310  fo1st  6325  f1stres  6327  bropopvvv  6385  errn  6886  xpassen  7161  xpdom2  7162  oicl  7454  oif  7455  hartogslem1  7467  cantnfdm  7575  cantnfval  7579  cantnf0  7586  cantnfres  7589  cnfcomlem  7612  hsmexlem4  8265  hsmexlem5  8266  axdc3lem2  8287  ttukeylem3  8347  hashfun  11655  swrdval  11719  s4dom  11821  shftdm  11841  rlim  12244  ramval  13331  isstruct2  13433  setsvalg  13447  prdsval  13633  homfeqbas  13877  invf  13948  oppciso  13957  sscfn1  13972  sscfn2  13973  isssc  13975  rescval  13982  rescval2  13983  issubc  13990  issubc2  13991  cofuval  14034  resfval  14044  resfval2  14045  resf1st  14046  prfval  14251  gsumvalx  14729  cntzrcl  15081  dmdprd  15514  dprdval  15516  dpjfval  15568  ablfaclem3  15600  elocv  16850  ishil  16900  iscnp2  17257  ptval  17555  ptcmplem2  18037  cnextfval  18046  tsmsval2  18112  ustbas2  18208  utopval  18215  tusval  18249  ucnval  18260  iscfilu  18271  psmetdmdm  18289  xmetdmdm  18318  blfvalps  18366  setsmstopn  18461  tmsval  18464  metuvalOLD  18532  metuval  18533  tngtopn  18644  cfilfval  19170  caufval  19181  limcfval  19712  dvfval  19737  dvbsss  19742  perfdvf  19743  dvn2bss  19769  dvnres  19770  dvcmul  19783  dvcmulf  19784  dvcj  19789  dvnfre  19791  dvexp  19792  dvmptres3  19795  dvmptcl  19798  dvmptadd  19799  dvmptmul  19800  dvmptres2  19801  dvmptcmul  19803  dvmptcj  19807  dvmptco  19811  rolle  19827  cmvth  19828  mvth  19829  dvlip  19830  dvlipcn  19831  dvlip2  19832  c1liplem1  19833  dveq0  19837  dv11cn  19838  dvle  19844  dvivthlem1  19845  dvivth  19847  dvne0  19848  lhop1lem  19850  lhop2  19852  lhop  19853  dvcnvrelem1  19854  dvcvx  19857  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvmptrecl  19861  dvfsumlem2  19864  itgsubstlem  19885  mpfrcl  19892  taylfval  20228  tayl0  20231  dvtaylp  20239  dvntaylp  20240  dvntaylp0  20241  taylthlem1  20242  taylthlem2  20243  ulmdvlem1  20269  pserdv  20298  pige3  20378  logtayl  20504  isumgra  21303  vdgrfval  21619  iseupa  21640  grporndm  21751  isabloda  21840  isass  21857  isexid  21858  ismndo2  21886  rngodm1dm2  21959  vcoprne  22011  hmoval  22264  metidval  24238  pstmval  24243  ofcfval  24434  ofcfval3  24438  brae  24545  braew  24546  faeval  24550  mbfmcst  24562  issibf  24601  sitmval  24614  0rrv  24662  dstrvprob  24682  lgamgulmlem2  24767  relexpdm  25088  areacirclem3  26182  sdclem2  26336  ismtyval  26399  exidreslem  26442  divrngcl  26463  isdrngo2  26464  fninfp  26625  fndifnfp  26627  dsmmval  27068  f1omvdco2  27259  pmtrfrn  27268  symgsssg  27276  symgfisg  27277  symggen  27279  psgnunilem1  27284  psgnunilem5  27285  psgnunilem2  27286  psgnunilem3  27287  psgneldm  27294  dvsconst  27415  expgrowth  27420  itgsinexplem1  27615  dfateq12d  27860  2wlkonot3v  28072  2spthonot3v  28073  dibffval  31623  dibfval  31624
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-dm 4847
  Copyright terms: Public domain W3C validator