Theorem dmeqd 5896

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

Syntax hints:   → wi 4   = wceq 1567  dom cdm 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-dm 5672

This theorem is referenced by:  dmxpid  5921  rneq  5927  dmxpss  6170  dmsnopss  6216  dmsnsnsn  6222  f10d  6856  fndmin  7041  fninfp  7173  fndifnfp  7175  ovmpt3rabdm  7670  elxp4  7918  1stval  7987  fo1st  8005  f1stres  8009  bropopvvv  8084  bropfvvvv  8086  mpocurryd  8264  errn  8716  xpassen  9058  xpdom2  9059  oicl  9490  oif  9491  hartogslem1  9503  cantnfdm  9632  cantnfval  9636  cantnf0  9643  cantnfres  9645  cnfcomlem  9667  hsmexlem4  10412  hsmexlem5  10413  axdc3lem2  10434  ttukeylem3  10494  hashfun  14473  s1dmALT  14646  swrdval  14680  swrd0  14695  s2dmALT  14944  s4dom  14955  dmtrclfv  15054  relexpnndm  15077  relexpdmg  15078  relexpdmd  15080  relexpnnrn  15081  relexpfld  15085  relexpaddg  15089  shftdm  15107  rlim  15545  ramval  17067  isstruct2  17208  setsvalg  17225  setsdm  17229  prdsval  17507  homfeqbas  17751  invf  17824  dfiso2  17828  oppciso  17837  cicsym  17860  sscfn1  17873  sscfn2  17874  isssc  17876  rescval  17883  rescval2  17884  issubc  17891  issubc2  17892  cofuval  17938  resfval  17948  resfval2  17949  resf1st  17950  estrreslem2  18193  prfval  18254  lubdm  18404  glbdm  18417  joindm  18428  meetdm  18442  islat  18488  isclat  18555  oduclatb  18562  gsumvalx  18733  mndpsuppss  18822  cntzrcl  19396  f1omvdco2  19517  pmtrfrn  19527  symgsssg  19536  symgfisg  19537  symggen  19539  pmtrdifwrdellem3  19552  pmtrdifwrdel2lem1  19553  pmtrdifwrdel  19554  pmtrdifwrdel2  19555  psgnunilem1  19562  psgnunilem5  19563  psgnunilem2  19564  psgnunilem3  19565  psgneldm  19572  dmdprd  20069  dprdval  20074  dpjfval  20126  ablfaclem3  20158  cofipsgn  21711  elocv  21786  ishil  21836  dsmmval  21852  mpfrcl  22204  mamudm  22520  mavmuldm  22675  mavmul0g  22678  m1detdiag  22722  decpmatval0  22889  decpmatval  22890  pmatcollpw3lem  22908  iscnp2  23364  ptval  23695  ptcmplem2  24178  cnextfval  24187  tsmsval2  24255  ustbas2  24350  utopval  24357  tusval  24390  ucnval  24401  iscfilu  24412  psmetdmdm  24430  xmetdmdm  24460  blfvalps  24508  setsmstopn  24603  tmsval  24606  metuval  24674  tngtopn  24775  cfilfval  25391  caufval  25402  limcfval  25999  dvfval  26024  dvbsss  26029  perfdvf  26030  dvmptresicc  26043  dvn2bss  26057  dvnres  26058  dvcmul  26071  dvcmulf  26072  dvcj  26077  dvnfre  26079  dvexp  26080  dvmptres3  26083  dvmptcl  26086  dvmptadd  26087  dvmptmul  26088  dvmptres2  26089  dvmptcmul  26091  dvmptcj  26095  dvmptco  26099  rolle  26117  cmvth  26118  mvth  26119  dvlip  26120  dvlipcn  26121  dvlip2  26122  c1liplem1  26123  dveq0  26127  dv11cn  26128  dvle  26134  dvivthlem1  26135  dvivth  26137  dvne0  26138  lhop1lem  26140  lhop2  26142  lhop  26143  dvcnvrelem1  26144  dvcvx  26147  dvfsumle  26148  dvfsumge  26149  dvfsumabs  26150  dvmptrecl  26151  dvfsumlem2  26154  itgsubstlem  26175  taylfval  26487  tayl0  26490  dvtaylp  26498  dvntaylp  26499  dvntaylp0  26500  taylthlem1  26501  taylthlem2  26502  ulmdvlem1  26528  pserdv  26557  pige3ALT  26650  logtayl  26790  relogbf  26921  lgamgulmlem2  27159  nosupdm  27833  nosupbday  27834  nosupres  27836  nosupbnd1lem1  27837  nosupbnd1  27843  nosupbnd2  27845  noinfdm  27848  noinfbday  27849  noinfbnd1  27858  noinfbnd2  27860  perpln1  28948  isuhgr  29350  isushgr  29351  uhgreq12g  29355  isuhgrop  29360  uhgrun  29364  uhgrstrrepe  29368  isupgr  29374  upgrop  29384  isumgr  29385  upgr1e  29403  upgrun  29408  umgrun  29410  isuspgr  29442  isusgr  29443  isuspgrop  29451  isusgrop  29452  ausgrusgrb  29455  usgrstrrepe  29525  uspgr1e  29534  issubgr  29561  uhgrspansubgrlem  29580  usgrexi  29731  vtxdgfval  29757  vtxdeqd  29767  vtxdun  29771  1loopgrvd0  29794  1hevtxdg0  29795  1hevtxdg1  29796  umgr2v2e  29815  umgr2v2evd2  29817  ewlksfval  29891  wksfval  29899  wlkres  29958  wlkp1  29969  eupths  30491  eupthres  30506  trlsegvdeglem4  30514  trlsegvdeglem5  30515  grporndm  30802  hmoval  31102  gsumhashmul  33327  symgcom2  33344  symgcntz  33345  pmtrcnel2  33350  cycpmco2f1  33384  cycpmrn  33403  tocyccntz  33404  fxpval  33425  fxpgaval  33427  1arithidomlem2  33770  1arithidom  33771  minplyval  34039  smatrcl  34130  metidval  34224  pstmval  34229  prsssdm  34251  ordtrestNEW  34255  ofcfval  34432  ofcfval3  34436  brae  34575  braew  34576  faeval  34580  mbfmcst  34593  carsgval  34637  issibf  34667  sitmval  34683  0rrv  34785  dstrvprob  34806  fineqvac  35451  satfdm  35759  fmlafv  35770  fmla  35771  fmlasuc0  35774  satfdmfmla  35790  cnndvlem2  37015  bj-finsumval0  37816  cureq  38134  curf  38136  curunc  38140  sdclem2  38280  ismtyval  38338  isass  38384  isexid  38385  ismndo2  38412  exidreslem  38415  rngodm1dm2  38470  divrngcl  38495  isdrngo2  38496  cnvref4  38888  isopos  39843  isatl  39962  dibffval  41803  dibfval  41804  conrel2d  44281  iunrelexp0  44319  dmtrclfvRP  44347  rntrclfvRP  44348  neicvgbex  44729  dvsconst  44931  expgrowth  44936  fnlimfvre  46279  dvsinax  46518  dvcosax  46531  dvbdfbdioolem1  46533  itgsinexplem1  46559  itgcoscmulx  46574  dirkeritg  46707  dirkercncflem2  46709  fourierdlem60  46771  fourierdlem61  46772  fourierdlem74  46785  fourierdlem75  46786  fourierdlem80  46791  fourierdlem94  46805  fourierdlem103  46814  fourierdlem104  46815  fourierdlem113  46824  dmvon  47211  ovnovollem1  47261  smflimlem3  47378  smflimlem4  47379  smflim  47382  smflim2  47411  smfpimcc  47413  smflimmpt  47415  smfsuplem2  47417  smfsuplem3  47418  smfsup  47419  smfsupmpt  47420  smfinflem  47422  smfinf  47423  smfinfmpt  47424  smflimsuplem1  47425  smflimsuplem2  47426  smflimsuplem3  47427  smflimsuplem4  47428  smflimsuplem7  47431  smflimsup  47433  smflimsupmpt  47434  smfliminf  47436  smfliminfmpt  47437  dfateq12d  47751  isubgruhgr  48521  grimidvtxedg  48538  ushggricedg  48580  isubgrgrim  48582  stgrusgra  48612  gpgiedgdmel  48702  gpgusgra  48710  upwlksfval  48788  dmrnxp  49499  lubeldm2d  49620  glbeldm2d  49621  glbprlem  49627  isclatd  49645  isopropdlem  49702  dmdm  49715  infsubc2  49723  infsubc2d  49724  oppfvalg  49788  reldmprcof1  50043  reldmprcof2  50044  dfinito4  50163  reldmlan2  50279  reldmran2  50280  termolmd  50332