Theorem dmeqd 5859

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 5857	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐴 = dom 𝐵)

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-dm 5641

This theorem is referenced by:  dmxpid  5883  rneq  5889  dmxpss  6132  dmsnopss  6175  dmsnsnsn  6181  f10d  6816  fndmin  6999  fninfp  7130  fndifnfp  7132  ovmpt3rabdm  7628  elxp4  7878  1stval  7949  fo1st  7967  f1stres  7971  bropopvvv  8046  bropfvvvv  8048  mpocurryd  8225  errn  8670  xpassen  9012  xpdom2  9013  oicl  9458  oif  9459  hartogslem1  9471  cantnfdm  9593  cantnfval  9597  cantnf0  9604  cantnfres  9606  cnfcomlem  9628  hsmexlem4  10358  hsmexlem5  10359  axdc3lem2  10380  ttukeylem3  10440  hashfun  14378  s1dmALT  14550  swrdval  14584  swrd0  14599  s2dmALT  14850  s4dom  14861  dmtrclfv  14960  relexpnndm  14983  relexpdmg  14984  relexpdmd  14986  relexpnnrn  14987  relexpfld  14991  relexpaddg  14995  shftdm  15013  rlim  15437  ramval  16955  isstruct2  17095  setsvalg  17112  setsdm  17116  prdsval  17394  homfeqbas  17637  invf  17710  dfiso2  17714  oppciso  17723  cicsym  17746  sscfn1  17759  sscfn2  17760  isssc  17762  rescval  17769  rescval2  17770  issubc  17777  issubc2  17778  cofuval  17824  resfval  17834  resfval2  17835  resf1st  17836  estrreslem2  18079  prfval  18140  lubdm  18290  glbdm  18303  joindm  18314  meetdm  18328  islat  18374  isclat  18441  oduclatb  18448  gsumvalx  18585  mndpsuppss  18674  cntzrcl  19241  f1omvdco2  19362  pmtrfrn  19372  symgsssg  19381  symgfisg  19382  symggen  19384  pmtrdifwrdellem3  19397  pmtrdifwrdel2lem1  19398  pmtrdifwrdel  19399  pmtrdifwrdel2  19400  psgnunilem1  19407  psgnunilem5  19408  psgnunilem2  19409  psgnunilem3  19410  psgneldm  19417  dmdprd  19914  dprdval  19919  dpjfval  19971  ablfaclem3  20003  cofipsgn  21535  elocv  21610  ishil  21660  dsmmval  21676  mpfrcl  22025  mamudm  22315  mavmuldm  22470  mavmul0g  22473  m1detdiag  22517  decpmatval0  22684  decpmatval  22685  pmatcollpw3lem  22703  iscnp2  23159  ptval  23490  ptcmplem2  23973  cnextfval  23982  tsmsval2  24050  ustbas2  24146  utopval  24153  tusval  24186  ucnval  24197  iscfilu  24208  psmetdmdm  24226  xmetdmdm  24256  blfvalps  24304  setsmstopn  24399  tmsval  24402  metuval  24470  tngtopn  24571  cfilfval  25197  caufval  25208  limcfval  25806  dvfval  25831  dvbsss  25836  perfdvf  25837  dvmptresicc  25850  dvn2bss  25865  dvnres  25866  dvcmul  25880  dvcmulf  25881  dvcj  25887  dvnfre  25889  dvexp  25890  dvmptres3  25893  dvmptcl  25896  dvmptadd  25897  dvmptmul  25898  dvmptres2  25899  dvmptcmul  25901  dvmptcj  25905  dvmptco  25909  rolle  25927  cmvth  25928  cmvthOLD  25929  mvth  25930  dvlip  25931  dvlipcn  25932  dvlip2  25933  c1liplem1  25934  dveq0  25938  dv11cn  25939  dvle  25945  dvivthlem1  25946  dvivth  25948  dvne0  25949  lhop1lem  25951  lhop2  25953  lhop  25954  dvcnvrelem1  25955  dvcvx  25958  dvfsumle  25959  dvfsumleOLD  25960  dvfsumge  25961  dvfsumabs  25962  dvmptrecl  25963  dvfsumlem2  25966  dvfsumlem2OLD  25967  itgsubstlem  25988  taylfval  26299  tayl0  26302  dvtaylp  26311  dvntaylp  26312  dvntaylp0  26313  taylthlem1  26314  taylthlem2  26315  taylthlem2OLD  26316  ulmdvlem1  26342  pserdv  26372  pige3ALT  26462  logtayl  26602  relogbf  26734  lgamgulmlem2  26973  nosupdm  27649  nosupbday  27650  nosupres  27652  nosupbnd1lem1  27653  nosupbnd1  27659  nosupbnd2  27661  noinfdm  27664  noinfbday  27665  noinfbnd1  27674  noinfbnd2  27676  perpln1  28690  isuhgr  29040  isushgr  29041  uhgreq12g  29045  isuhgrop  29050  uhgrun  29054  uhgrstrrepe  29058  isupgr  29064  upgrop  29074  isumgr  29075  upgr1e  29093  upgrun  29098  umgrun  29100  isuspgr  29132  isusgr  29133  isuspgrop  29141  isusgrop  29142  ausgrusgrb  29145  usgrstrrepe  29215  uspgr1e  29224  issubgr  29251  uhgrspansubgrlem  29270  usgrexi  29421  vtxdgfval  29448  vtxdeqd  29458  vtxdun  29462  1loopgrvd0  29485  1hevtxdg0  29486  1hevtxdg1  29487  umgr2v2e  29506  umgr2v2evd2  29508  ewlksfval  29582  wksfval  29590  wlkres  29649  wlkp1  29660  eupths  30179  eupthres  30194  trlsegvdeglem4  30202  trlsegvdeglem5  30203  grporndm  30489  hmoval  30789  gsumhashmul  33044  symgcom2  33056  symgcntz  33057  pmtrcnel2  33062  cycpmco2f1  33096  cycpmrn  33115  tocyccntz  33116  fxpval  33137  fxpgaval  33139  1arithidomlem2  33500  1arithidom  33501  minplyval  33688  smatrcl  33779  metidval  33873  pstmval  33878  prsssdm  33900  ordtrestNEW  33904  ofcfval  34081  ofcfval3  34085  brae  34224  braew  34225  faeval  34229  mbfmcst  34243  carsgval  34287  issibf  34317  sitmval  34333  0rrv  34435  dstrvprob  34456  fineqvac  35080  satfdm  35349  fmlafv  35360  fmla  35361  fmlasuc0  35364  satfdmfmla  35380  cnndvlem2  36519  bj-finsumval0  37266  cureq  37583  curf  37585  curunc  37589  sdclem2  37729  ismtyval  37787  isass  37833  isexid  37834  ismndo2  37861  exidreslem  37864  rngodm1dm2  37919  divrngcl  37944  isdrngo2  37945  cnvref4  38325  isopos  39166  isatl  39285  dibffval  41127  dibfval  41128  conrel2d  43646  iunrelexp0  43684  dmtrclfvRP  43712  rntrclfvRP  43713  neicvgbex  44094  dvsconst  44312  expgrowth  44317  fnlimfvre  45665  dvsinax  45904  dvcosax  45917  dvbdfbdioolem1  45919  itgsinexplem1  45945  itgcoscmulx  45960  dirkeritg  46093  dirkercncflem2  46095  fourierdlem60  46157  fourierdlem61  46158  fourierdlem74  46171  fourierdlem75  46172  fourierdlem80  46177  fourierdlem94  46191  fourierdlem103  46200  fourierdlem104  46201  fourierdlem113  46210  dmvon  46597  ovnovollem1  46647  smflimlem3  46764  smflimlem4  46765  smflim  46768  smflim2  46797  smfpimcc  46799  smflimmpt  46801  smfsuplem2  46803  smfsuplem3  46804  smfsup  46805  smfsupmpt  46806  smfinflem  46808  smfinf  46809  smfinfmpt  46810  smflimsuplem1  46811  smflimsuplem2  46812  smflimsuplem3  46813  smflimsuplem4  46814  smflimsuplem7  46817  smflimsup  46819  smflimsupmpt  46820  smfliminf  46822  smfliminfmpt  46823  dfateq12d  47120  isubgruhgr  47861  grimidvtxedg  47878  ushggricedg  47920  isubgrgrim  47922  stgrusgra  47951  gpgiedgdmel  48033  gpgusgra  48041  upwlksfval  48116  dmrnxp  48818  lubeldm2d  48939  glbeldm2d  48940  glbprlem  48946  isclatd  48964  isopropdlem  49022  dmdm  49035  infsubc2  49043  infsubc2d  49044  oppfvalg  49108  reldmprcof1  49363  reldmprcof2  49364  dfinito4  49483  reldmlan2  49599  reldmran2  49600  termolmd  49652