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

Theorem dmeqd 5025
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 5023 . 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 1405   dom cdm 4822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-dm 4832
This theorem is referenced by:  dmxpid  5042  rneq  5048  dmxpss  5255  dmsnopss  5295  dmsnsnsn  5301  fndmin  5971  fninfp  6077  fndifnfp  6079  ovmpt3rabdm  6515  elxp4  6727  1stval  6785  fo1st  6803  f1stres  6805  bropopvvv  6863  suppsnop  6915  mpt2curryd  7000  errn  7369  xpassen  7648  xpdom2  7649  oicl  7987  oif  7988  hartogslem1  8000  cantnfdm  8112  cantnfdmOLD  8114  cantnfval  8118  cantnf0  8125  cantnfres  8127  cantnfvalOLD  8148  cnfcomlem  8174  cnfcomlemOLD  8182  hsmexlem4  8840  hsmexlem5  8841  axdc3lem2  8862  ttukeylem3  8922  hashfun  12542  swrdval  12696  swrd0  12713  s4dom  12921  dmtrclfv  12999  relexpnndm  13021  relexpdmg  13022  relexpnnrn  13025  relexpfld  13029  relexpaddg  13033  shftdm  13051  rlim  13465  ramval  14733  isstruct2  14848  setsvalg  14863  prdsval  15067  homfeqbas  15307  invf  15379  dfiso2  15383  oppciso  15392  cicsym  15415  sscfn1  15428  sscfn2  15429  isssc  15431  rescval  15438  rescval2  15439  issubc  15446  issubc2  15447  cofuval  15493  resfval  15503  resfval2  15504  resf1st  15505  estrreslem2  15729  prfval  15790  lubdm  15931  glbdm  15944  joindm  15955  meetdm  15969  islat  15999  isclat  16061  oduclatb  16096  gsumvalx  16219  cntzrcl  16687  f1omvdco2  16795  pmtrfrn  16805  symgsssg  16814  symgfisg  16815  symggen  16817  pmtrdifwrdellem3  16830  pmtrdifwrdel2lem1  16831  pmtrdifwrdel  16832  pmtrdifwrdel2  16833  psgnunilem1  16840  psgnunilem5  16841  psgnunilem2  16842  psgnunilem3  16843  psgneldm  16850  dmdprd  17347  dprdval  17352  dprdvalOLD  17354  dpjfval  17422  ablfaclem3  17456  mpfrcl  18505  zrhcofipsgn  18925  elocv  18995  ishil  19045  dsmmval  19061  mamudm  19180  mavmuldm  19342  mavmul0g  19345  m1detdiag  19389  decpmatval0  19555  decpmatval  19556  pmatcollpw3lem  19574  iscnp2  20031  ptval  20361  ptcmplem2  20843  cnextfval  20852  tsmsval2  20918  ustbas2  21018  utopval  21025  tusval  21059  ucnval  21070  iscfilu  21081  psmetdmdm  21099  xmetdmdm  21128  blfvalps  21176  setsmstopn  21271  tmsval  21274  metuvalOLD  21342  metuval  21343  tngtopn  21454  cfilfval  21993  caufval  22004  limcfval  22566  dvfval  22591  dvbsss  22596  perfdvf  22597  dvn2bss  22623  dvnres  22624  dvcmul  22637  dvcmulf  22638  dvcj  22643  dvnfre  22645  dvexp  22646  dvmptres3  22649  dvmptcl  22652  dvmptadd  22653  dvmptmul  22654  dvmptres2  22655  dvmptcmul  22657  dvmptcj  22661  dvmptco  22665  rolle  22681  cmvth  22682  mvth  22683  dvlip  22684  dvlipcn  22685  dvlip2  22686  c1liplem1  22687  dveq0  22691  dv11cn  22692  dvle  22698  dvivthlem1  22699  dvivth  22701  dvne0  22702  lhop1lem  22704  lhop2  22706  lhop  22707  dvcnvrelem1  22708  dvcvx  22711  dvfsumle  22712  dvfsumge  22713  dvfsumabs  22714  dvmptrecl  22715  dvfsumlem2  22718  itgsubstlem  22739  taylfval  23044  tayl0  23047  dvtaylp  23055  dvntaylp  23056  dvntaylp0  23057  taylthlem1  23058  taylthlem2  23059  ulmdvlem1  23085  pserdv  23114  pige3  23200  logtayl  23333  relogbf  23456  lgamgulmlem2  23683  perpln1  24470  isushgra  24705  isumgra  24719  clwwlknprop  25176  2wlkonot3v  25279  2spthonot3v  25280  vdgrfval  25299  iseupa  25369  grporndm  25612  isabloda  25701  isass  25718  isexid  25719  ismndo2  25747  rngodm1dm2  25820  vcoprne  25872  hmoval  26125  metidval  28308  pstmval  28313  prsssdm  28338  ordtrestNEW  28342  ofcfval  28531  ofcfval3  28535  brae  28676  braew  28677  faeval  28681  mbfmcst  28693  carsgval  28737  issibf  28767  sitmval  28782  0rrv  28882  dstrvprob  28902  bj-finsumval0  31214  sdclem2  31497  ismtyval  31558  exidreslem  31601  divrngcl  31622  isdrngo2  31623  isopos  32178  isatl  32297  dibffval  34140  dibfval  34141  conrel2d  35623  iunrelexp0  35661  dmtrclfvRP  35689  rntrclfvRP  35690  dvsconst  36063  expgrowth  36068  dvsinax  37057  dvmptresicc  37065  dvcosax  37072  dvbdfbdioolem1  37074  itgsinexplem1  37101  itgcoscmulx  37117  dirkeritg  37233  dirkercncflem2  37235  fourierdlem60  37298  fourierdlem61  37299  fourierdlem74  37312  fourierdlem75  37313  fourierdlem80  37318  fourierdlem94  37332  fourierdlem103  37341  fourierdlem104  37342  fourierdlem113  37351  dfateq12d  37563  isuhgr  37976  isushgr  37977  uhgeq12g  37980  uhguhgra  37982  uhgrauhg  37983  uhgrepe  37988  gsizval  37999  gsizopval  38001  mndpsuppss  38456
  Copyright terms: Public domain W3C validator