Theorem dmeqd 5803

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-dm 5590

This theorem is referenced by:  dmxpid  5828  rneq  5834  dmxpss  6063  dmsnopss  6106  dmsnsnsn  6112  f10d  6733  fndmin  6904  fninfp  7028  fndifnfp  7030  ovmpt3rabdm  7506  elxp4  7743  1stval  7806  fo1st  7824  f1stres  7828  bropopvvv  7901  bropfvvvv  7903  mpocurryd  8056  errn  8478  xpassen  8806  xpdom2  8807  oicl  9218  oif  9219  hartogslem1  9231  cantnfdm  9352  cantnfval  9356  cantnf0  9363  cantnfres  9365  cnfcomlem  9387  hsmexlem4  10116  hsmexlem5  10117  axdc3lem2  10138  ttukeylem3  10198  hashfun  14080  s1dmALT  14242  swrdval  14284  swrd0  14299  s2dmALT  14549  s4dom  14560  dmtrclfv  14657  relexpnndm  14680  relexpdmg  14681  relexpdmd  14683  relexpnnrn  14684  relexpfld  14688  relexpaddg  14692  shftdm  14710  rlim  15132  ramval  16637  isstruct2  16778  setsvalg  16795  setsdm  16799  prdsval  17083  homfeqbas  17322  invf  17397  dfiso2  17401  oppciso  17410  cicsym  17433  sscfn1  17446  sscfn2  17447  isssc  17449  rescval  17456  rescval2  17457  issubc  17466  issubc2  17467  cofuval  17513  resfval  17523  resfval2  17524  resf1st  17525  estrreslem2  17771  prfval  17832  lubdm  17984  glbdm  17997  joindm  18008  meetdm  18022  islat  18066  isclat  18133  oduclatb  18140  gsumvalx  18275  cntzrcl  18848  f1omvdco2  18971  pmtrfrn  18981  symgsssg  18990  symgfisg  18991  symggen  18993  pmtrdifwrdellem3  19006  pmtrdifwrdel2lem1  19007  pmtrdifwrdel  19008  pmtrdifwrdel2  19009  psgnunilem1  19016  psgnunilem5  19017  psgnunilem2  19018  psgnunilem3  19019  psgneldm  19026  dmdprd  19516  dprdval  19521  dpjfval  19573  ablfaclem3  19605  cofipsgn  20710  elocv  20785  ishil  20835  dsmmval  20851  mpfrcl  21205  mamudm  21447  mavmuldm  21607  mavmul0g  21610  m1detdiag  21654  decpmatval0  21821  decpmatval  21822  pmatcollpw3lem  21840  iscnp2  22298  ptval  22629  ptcmplem2  23112  cnextfval  23121  tsmsval2  23189  ustbas2  23285  utopval  23292  tusval  23325  ucnval  23337  iscfilu  23348  psmetdmdm  23366  xmetdmdm  23396  blfvalps  23444  setsmstopn  23539  tmsval  23542  metuval  23611  tngtopn  23720  cfilfval  24333  caufval  24344  limcfval  24941  dvfval  24966  dvbsss  24971  perfdvf  24972  dvmptresicc  24985  dvn2bss  24999  dvnres  25000  dvcmul  25013  dvcmulf  25014  dvcj  25019  dvnfre  25021  dvexp  25022  dvmptres3  25025  dvmptcl  25028  dvmptadd  25029  dvmptmul  25030  dvmptres2  25031  dvmptcmul  25033  dvmptcj  25037  dvmptco  25041  rolle  25059  cmvth  25060  mvth  25061  dvlip  25062  dvlipcn  25063  dvlip2  25064  c1liplem1  25065  dveq0  25069  dv11cn  25070  dvle  25076  dvivthlem1  25077  dvivth  25079  dvne0  25080  lhop1lem  25082  lhop2  25084  lhop  25085  dvcnvrelem1  25086  dvcvx  25089  dvfsumle  25090  dvfsumge  25091  dvfsumabs  25092  dvmptrecl  25093  dvfsumlem2  25096  itgsubstlem  25117  taylfval  25423  tayl0  25426  dvtaylp  25434  dvntaylp  25435  dvntaylp0  25436  taylthlem1  25437  taylthlem2  25438  ulmdvlem1  25464  pserdv  25493  pige3ALT  25581  logtayl  25720  relogbf  25846  lgamgulmlem2  26084  perpln1  26975  isuhgr  27333  isushgr  27334  uhgreq12g  27338  isuhgrop  27343  uhgrun  27347  uhgrstrrepe  27351  isupgr  27357  upgrop  27367  isumgr  27368  upgr1e  27386  upgrun  27391  umgrun  27393  isuspgr  27425  isusgr  27426  isuspgrop  27434  isusgrop  27435  ausgrusgrb  27438  usgrstrrepe  27505  uspgr1e  27514  usgrexmpl  27533  issubgr  27541  uhgrspansubgrlem  27560  usgrexi  27711  vtxdgfval  27737  vtxdeqd  27747  vtxdun  27751  1loopgrvd0  27774  1hevtxdg0  27775  1hevtxdg1  27776  umgr2v2e  27795  umgr2v2evd2  27797  ewlksfval  27871  wksfval  27879  wlkres  27940  wlkp1  27951  eupths  28465  eupthres  28480  trlsegvdeglem4  28488  trlsegvdeglem5  28489  grporndm  28773  hmoval  29073  gsumhashmul  31218  symgcom2  31255  symgcntz  31256  pmtrcnel2  31261  cycpmco2f1  31293  cycpmrn  31312  tocyccntz  31313  smatrcl  31648  metidval  31742  pstmval  31747  prsssdm  31769  ordtrestNEW  31773  ofcfval  31966  ofcfval3  31970  brae  32109  braew  32110  faeval  32114  mbfmcst  32126  carsgval  32170  issibf  32200  sitmval  32216  0rrv  32318  dstrvprob  32338  fineqvac  32966  satfdm  33231  fmlafv  33242  fmla  33243  fmlasuc0  33246  satfdmfmla  33262  nosupdm  33834  nosupbday  33835  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1  33844  nosupbnd2  33846  noinfdm  33849  noinfbday  33850  noinfbnd1  33859  noinfbnd2  33861  cnndvlem2  34645  bj-finsumval0  35383  cureq  35680  curf  35682  curunc  35686  sdclem2  35827  ismtyval  35885  isass  35931  isexid  35932  ismndo2  35959  exidreslem  35962  rngodm1dm2  36017  divrngcl  36042  isdrngo2  36043  isopos  37121  isatl  37240  dibffval  39081  dibfval  39082  conrel2d  41161  iunrelexp0  41199  dmtrclfvRP  41227  rntrclfvRP  41228  neicvgbex  41611  dvsconst  41837  expgrowth  41842  fnlimfvre  43105  dvsinax  43344  dvcosax  43357  dvbdfbdioolem1  43359  itgsinexplem1  43385  itgcoscmulx  43400  dirkeritg  43533  dirkercncflem2  43535  fourierdlem60  43597  fourierdlem61  43598  fourierdlem74  43611  fourierdlem75  43612  fourierdlem80  43617  fourierdlem94  43631  fourierdlem103  43640  fourierdlem104  43641  fourierdlem113  43650  dmvon  44034  ovnovollem1  44084  smflimlem3  44195  smflimlem4  44196  smflim  44199  smflim2  44226  smfpimcc  44228  smflimmpt  44230  smfsuplem2  44232  smfsuplem3  44233  smfsup  44234  smfsupmpt  44235  smfinflem  44237  smfinf  44238  smfinfmpt  44239  smflimsuplem1  44240  smflimsuplem2  44241  smflimsuplem3  44242  smflimsuplem4  44243  smflimsuplem7  44246  smflimsup  44248  smflimsupmpt  44249  smfliminf  44251  smfliminfmpt  44252  dfateq12d  44505  isomgr  45163  isomgreqve  45165  ushrisomgr  45181  upwlksfval  45185  mndpsuppss  45595  lubeldm2d  46140  glbeldm2d  46141  glbprlem  46147  isclatd  46157