Theorem dmeqd 5848

Description: Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
dmeqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
dmeqd	⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Proof of Theorem dmeqd

Step	Hyp	Ref	Expression
1		dmeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dmeq 5846	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-dm 5629

This theorem is referenced by:  dmxpid  5872  rneq  5878  dmxpss  6120  dmsnopss  6163  dmsnsnsn  6169  f10d  6798  fndmin  6979  fninfp  7110  fndifnfp  7112  ovmpt3rabdm  7608  elxp4  7855  1stval  7926  fo1st  7944  f1stres  7948  bropopvvv  8023  bropfvvvv  8025  mpocurryd  8202  errn  8647  xpassen  8988  xpdom2  8989  oicl  9421  oif  9422  hartogslem1  9434  cantnfdm  9560  cantnfval  9564  cantnf0  9571  cantnfres  9573  cnfcomlem  9595  hsmexlem4  10323  hsmexlem5  10324  axdc3lem2  10345  ttukeylem3  10405  hashfun  14344  s1dmALT  14516  swrdval  14550  swrd0  14565  s2dmALT  14815  s4dom  14826  dmtrclfv  14925  relexpnndm  14948  relexpdmg  14949  relexpdmd  14951  relexpnnrn  14952  relexpfld  14956  relexpaddg  14960  shftdm  14978  rlim  15402  ramval  16920  isstruct2  17060  setsvalg  17077  setsdm  17081  prdsval  17359  homfeqbas  17602  invf  17675  dfiso2  17679  oppciso  17688  cicsym  17711  sscfn1  17724  sscfn2  17725  isssc  17727  rescval  17734  rescval2  17735  issubc  17742  issubc2  17743  cofuval  17789  resfval  17799  resfval2  17800  resf1st  17801  estrreslem2  18044  prfval  18105  lubdm  18255  glbdm  18268  joindm  18279  meetdm  18293  islat  18339  isclat  18406  oduclatb  18413  gsumvalx  18550  mndpsuppss  18639  cntzrcl  19206  f1omvdco2  19327  pmtrfrn  19337  symgsssg  19346  symgfisg  19347  symggen  19349  pmtrdifwrdellem3  19362  pmtrdifwrdel2lem1  19363  pmtrdifwrdel  19364  pmtrdifwrdel2  19365  psgnunilem1  19372  psgnunilem5  19373  psgnunilem2  19374  psgnunilem3  19375  psgneldm  19382  dmdprd  19879  dprdval  19884  dpjfval  19936  ablfaclem3  19968  cofipsgn  21500  elocv  21575  ishil  21625  dsmmval  21641  mpfrcl  21990  mamudm  22280  mavmuldm  22435  mavmul0g  22438  m1detdiag  22482  decpmatval0  22649  decpmatval  22650  pmatcollpw3lem  22668  iscnp2  23124  ptval  23455  ptcmplem2  23938  cnextfval  23947  tsmsval2  24015  ustbas2  24111  utopval  24118  tusval  24151  ucnval  24162  iscfilu  24173  psmetdmdm  24191  xmetdmdm  24221  blfvalps  24269  setsmstopn  24364  tmsval  24367  metuval  24435  tngtopn  24536  cfilfval  25162  caufval  25173  limcfval  25771  dvfval  25796  dvbsss  25801  perfdvf  25802  dvmptresicc  25815  dvn2bss  25830  dvnres  25831  dvcmul  25845  dvcmulf  25846  dvcj  25852  dvnfre  25854  dvexp  25855  dvmptres3  25858  dvmptcl  25861  dvmptadd  25862  dvmptmul  25863  dvmptres2  25864  dvmptcmul  25866  dvmptcj  25870  dvmptco  25874  rolle  25892  cmvth  25893  cmvthOLD  25894  mvth  25895  dvlip  25896  dvlipcn  25897  dvlip2  25898  c1liplem1  25899  dveq0  25903  dv11cn  25904  dvle  25910  dvivthlem1  25911  dvivth  25913  dvne0  25914  lhop1lem  25916  lhop2  25918  lhop  25919  dvcnvrelem1  25920  dvcvx  25923  dvfsumle  25924  dvfsumleOLD  25925  dvfsumge  25926  dvfsumabs  25927  dvmptrecl  25928  dvfsumlem2  25931  dvfsumlem2OLD  25932  itgsubstlem  25953  taylfval  26264  tayl0  26267  dvtaylp  26276  dvntaylp  26277  dvntaylp0  26278  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  ulmdvlem1  26307  pserdv  26337  pige3ALT  26427  logtayl  26567  relogbf  26699  lgamgulmlem2  26938  nosupdm  27614  nosupbday  27615  nosupres  27617  nosupbnd1lem1  27618  nosupbnd1  27624  nosupbnd2  27626  noinfdm  27629  noinfbday  27630  noinfbnd1  27639  noinfbnd2  27641  perpln1  28655  isuhgr  29005  isushgr  29006  uhgreq12g  29010  isuhgrop  29015  uhgrun  29019  uhgrstrrepe  29023  isupgr  29029  upgrop  29039  isumgr  29040  upgr1e  29058  upgrun  29063  umgrun  29065  isuspgr  29097  isusgr  29098  isuspgrop  29106  isusgrop  29107  ausgrusgrb  29110  usgrstrrepe  29180  uspgr1e  29189  issubgr  29216  uhgrspansubgrlem  29235  usgrexi  29386  vtxdgfval  29413  vtxdeqd  29423  vtxdun  29427  1loopgrvd0  29450  1hevtxdg0  29451  1hevtxdg1  29452  umgr2v2e  29471  umgr2v2evd2  29473  ewlksfval  29547  wksfval  29555  wlkres  29614  wlkp1  29625  eupths  30144  eupthres  30159  trlsegvdeglem4  30167  trlsegvdeglem5  30168  grporndm  30454  hmoval  30754  gsumhashmul  33014  symgcom2  33026  symgcntz  33027  pmtrcnel2  33032  cycpmco2f1  33066  cycpmrn  33085  tocyccntz  33086  fxpval  33107  fxpgaval  33109  1arithidomlem2  33473  1arithidom  33474  minplyval  33672  smatrcl  33763  metidval  33857  pstmval  33862  prsssdm  33884  ordtrestNEW  33888  ofcfval  34065  ofcfval3  34069  brae  34208  braew  34209  faeval  34213  mbfmcst  34227  carsgval  34271  issibf  34301  sitmval  34317  0rrv  34419  dstrvprob  34440  fineqvac  35072  satfdm  35342  fmlafv  35353  fmla  35354  fmlasuc0  35357  satfdmfmla  35373  cnndvlem2  36512  bj-finsumval0  37259  cureq  37576  curf  37578  curunc  37582  sdclem2  37722  ismtyval  37780  isass  37826  isexid  37827  ismndo2  37854  exidreslem  37857  rngodm1dm2  37912  divrngcl  37937  isdrngo2  37938  cnvref4  38318  isopos  39159  isatl  39278  dibffval  41119  dibfval  41120  conrel2d  43637  iunrelexp0  43675  dmtrclfvRP  43703  rntrclfvRP  43704  neicvgbex  44085  dvsconst  44303  expgrowth  44308  fnlimfvre  45655  dvsinax  45894  dvcosax  45907  dvbdfbdioolem1  45909  itgsinexplem1  45935  itgcoscmulx  45950  dirkeritg  46083  dirkercncflem2  46085  fourierdlem60  46147  fourierdlem61  46148  fourierdlem74  46161  fourierdlem75  46162  fourierdlem80  46167  fourierdlem94  46181  fourierdlem103  46190  fourierdlem104  46191  fourierdlem113  46200  dmvon  46587  ovnovollem1  46637  smflimlem3  46754  smflimlem4  46755  smflim  46758  smflim2  46787  smfpimcc  46789  smflimmpt  46791  smfsuplem2  46793  smfsuplem3  46794  smfsup  46795  smfsupmpt  46796  smfinflem  46798  smfinf  46799  smfinfmpt  46800  smflimsuplem1  46801  smflimsuplem2  46802  smflimsuplem3  46803  smflimsuplem4  46804  smflimsuplem7  46807  smflimsup  46809  smflimsupmpt  46810  smfliminf  46812  smfliminfmpt  46813  dfateq12d  47110  isubgruhgr  47852  grimidvtxedg  47869  ushggricedg  47911  isubgrgrim  47913  stgrusgra  47943  gpgiedgdmel  48033  gpgusgra  48041  upwlksfval  48119  dmrnxp  48821  lubeldm2d  48942  glbeldm2d  48943  glbprlem  48949  isclatd  48967  isopropdlem  49025  dmdm  49038  infsubc2  49046  infsubc2d  49047  oppfvalg  49111  reldmprcof1  49366  reldmprcof2  49367  dfinito4  49486  reldmlan2  49602  reldmran2  49603  termolmd  49655