Theorem dmeqd 5885

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-dm 5664

This theorem is referenced by:  dmxpid  5910  rneq  5916  dmxpss  6160  dmsnopss  6203  dmsnsnsn  6209  f10d  6851  fndmin  7034  fninfp  7165  fndifnfp  7167  ovmpt3rabdm  7664  elxp4  7916  1stval  7988  fo1st  8006  f1stres  8010  bropopvvv  8087  bropfvvvv  8089  mpocurryd  8266  errn  8739  xpassen  9078  xpdom2  9079  oicl  9541  oif  9542  hartogslem1  9554  cantnfdm  9676  cantnfval  9680  cantnf0  9687  cantnfres  9689  cnfcomlem  9711  hsmexlem4  10441  hsmexlem5  10442  axdc3lem2  10463  ttukeylem3  10523  hashfun  14453  s1dmALT  14625  swrdval  14659  swrd0  14674  s2dmALT  14925  s4dom  14936  dmtrclfv  15035  relexpnndm  15058  relexpdmg  15059  relexpdmd  15061  relexpnnrn  15062  relexpfld  15066  relexpaddg  15070  shftdm  15088  rlim  15509  ramval  17026  isstruct2  17166  setsvalg  17183  setsdm  17187  prdsval  17467  homfeqbas  17706  invf  17779  dfiso2  17783  oppciso  17792  cicsym  17815  sscfn1  17828  sscfn2  17829  isssc  17831  rescval  17838  rescval2  17839  issubc  17846  issubc2  17847  cofuval  17893  resfval  17903  resfval2  17904  resf1st  17905  estrreslem2  18148  prfval  18209  lubdm  18359  glbdm  18372  joindm  18383  meetdm  18397  islat  18441  isclat  18508  oduclatb  18515  gsumvalx  18652  mndpsuppss  18741  cntzrcl  19308  f1omvdco2  19427  pmtrfrn  19437  symgsssg  19446  symgfisg  19447  symggen  19449  pmtrdifwrdellem3  19462  pmtrdifwrdel2lem1  19463  pmtrdifwrdel  19464  pmtrdifwrdel2  19465  psgnunilem1  19472  psgnunilem5  19473  psgnunilem2  19474  psgnunilem3  19475  psgneldm  19482  dmdprd  19979  dprdval  19984  dpjfval  20036  ablfaclem3  20068  cofipsgn  21551  elocv  21626  ishil  21676  dsmmval  21692  mpfrcl  22041  mamudm  22331  mavmuldm  22486  mavmul0g  22489  m1detdiag  22533  decpmatval0  22700  decpmatval  22701  pmatcollpw3lem  22719  iscnp2  23175  ptval  23506  ptcmplem2  23989  cnextfval  23998  tsmsval2  24066  ustbas2  24162  utopval  24169  tusval  24202  ucnval  24213  iscfilu  24224  psmetdmdm  24242  xmetdmdm  24272  blfvalps  24320  setsmstopn  24415  tmsval  24418  metuval  24486  tngtopn  24587  cfilfval  25214  caufval  25225  limcfval  25823  dvfval  25848  dvbsss  25853  perfdvf  25854  dvmptresicc  25867  dvn2bss  25882  dvnres  25883  dvcmul  25897  dvcmulf  25898  dvcj  25904  dvnfre  25906  dvexp  25907  dvmptres3  25910  dvmptcl  25913  dvmptadd  25914  dvmptmul  25915  dvmptres2  25916  dvmptcmul  25918  dvmptcj  25922  dvmptco  25926  rolle  25944  cmvth  25945  cmvthOLD  25946  mvth  25947  dvlip  25948  dvlipcn  25949  dvlip2  25950  c1liplem1  25951  dveq0  25955  dv11cn  25956  dvle  25962  dvivthlem1  25963  dvivth  25965  dvne0  25966  lhop1lem  25968  lhop2  25970  lhop  25971  dvcnvrelem1  25972  dvcvx  25975  dvfsumle  25976  dvfsumleOLD  25977  dvfsumge  25978  dvfsumabs  25979  dvmptrecl  25980  dvfsumlem2  25983  dvfsumlem2OLD  25984  itgsubstlem  26005  taylfval  26316  tayl0  26319  dvtaylp  26328  dvntaylp  26329  dvntaylp0  26330  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmdvlem1  26359  pserdv  26389  pige3ALT  26479  logtayl  26619  relogbf  26751  lgamgulmlem2  26990  nosupdm  27666  nosupbday  27667  nosupres  27669  nosupbnd1lem1  27670  nosupbnd1  27676  nosupbnd2  27678  noinfdm  27681  noinfbday  27682  noinfbnd1  27691  noinfbnd2  27693  perpln1  28635  isuhgr  28985  isushgr  28986  uhgreq12g  28990  isuhgrop  28995  uhgrun  28999  uhgrstrrepe  29003  isupgr  29009  upgrop  29019  isumgr  29020  upgr1e  29038  upgrun  29043  umgrun  29045  isuspgr  29077  isusgr  29078  isuspgrop  29086  isusgrop  29087  ausgrusgrb  29090  usgrstrrepe  29160  uspgr1e  29169  issubgr  29196  uhgrspansubgrlem  29215  usgrexi  29366  vtxdgfval  29393  vtxdeqd  29403  vtxdun  29407  1loopgrvd0  29430  1hevtxdg0  29431  1hevtxdg1  29432  umgr2v2e  29451  umgr2v2evd2  29453  ewlksfval  29527  wksfval  29535  wlkres  29596  wlkp1  29607  eupths  30127  eupthres  30142  trlsegvdeglem4  30150  trlsegvdeglem5  30151  grporndm  30437  hmoval  30737  gsumhashmul  33001  symgcom2  33041  symgcntz  33042  pmtrcnel2  33047  cycpmco2f1  33081  cycpmrn  33100  tocyccntz  33101  1arithidomlem2  33497  1arithidom  33498  minplyval  33685  smatrcl  33773  metidval  33867  pstmval  33872  prsssdm  33894  ordtrestNEW  33898  ofcfval  34075  ofcfval3  34079  brae  34218  braew  34219  faeval  34223  mbfmcst  34237  carsgval  34281  issibf  34311  sitmval  34327  0rrv  34429  dstrvprob  34450  fineqvac  35074  satfdm  35337  fmlafv  35348  fmla  35349  fmlasuc0  35352  satfdmfmla  35368  cnndvlem2  36502  bj-finsumval0  37249  cureq  37566  curf  37568  curunc  37572  sdclem2  37712  ismtyval  37770  isass  37816  isexid  37817  ismndo2  37844  exidreslem  37847  rngodm1dm2  37902  divrngcl  37927  isdrngo2  37928  cnvref4  38314  isopos  39144  isatl  39263  dibffval  41105  dibfval  41106  conrel2d  43635  iunrelexp0  43673  dmtrclfvRP  43701  rntrclfvRP  43702  neicvgbex  44083  dvsconst  44302  expgrowth  44307  fnlimfvre  45651  dvsinax  45890  dvcosax  45903  dvbdfbdioolem1  45905  itgsinexplem1  45931  itgcoscmulx  45946  dirkeritg  46079  dirkercncflem2  46081  fourierdlem60  46143  fourierdlem61  46144  fourierdlem74  46157  fourierdlem75  46158  fourierdlem80  46163  fourierdlem94  46177  fourierdlem103  46186  fourierdlem104  46187  fourierdlem113  46196  dmvon  46583  ovnovollem1  46633  smflimlem3  46750  smflimlem4  46751  smflim  46754  smflim2  46783  smfpimcc  46785  smflimmpt  46787  smfsuplem2  46789  smfsuplem3  46790  smfsup  46791  smfsupmpt  46792  smfinflem  46794  smfinf  46795  smfinfmpt  46796  smflimsuplem1  46797  smflimsuplem2  46798  smflimsuplem3  46799  smflimsuplem4  46800  smflimsuplem7  46803  smflimsup  46805  smflimsupmpt  46806  smfliminf  46808  smfliminfmpt  46809  dfateq12d  47103  isubgruhgr  47829  grimidvtxedg  47846  ushggricedg  47888  isubgrgrim  47890  stgrusgra  47919  gpgiedgdmel  48001  gpgusgra  48009  upwlksfval  48058  dmrnxp  48763  lubeldm2d  48880  glbeldm2d  48881  glbprlem  48887  isclatd  48905  isopropdlem  48955  dmdm  48968  infsubc2  48976  infsubc2d  48977  oppfvalg  49022  reldmprcof1  49239  reldmprcof2  49240  dfinito4  49334  reldmlan2  49440  reldmran2  49441