Theorem dmeqd 5852

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-dm 5632

This theorem is referenced by:  dmxpid  5877  rneq  5883  dmxpss  6127  dmsnopss  6170  dmsnsnsn  6176  f10d  6806  fndmin  6988  fninfp  7118  fndifnfp  7120  ovmpt3rabdm  7615  elxp4  7862  1stval  7933  fo1st  7951  f1stres  7955  bropopvvv  8030  bropfvvvv  8032  mpocurryd  8209  errn  8655  xpassen  8997  xpdom2  8998  oicl  9432  oif  9433  hartogslem1  9445  cantnfdm  9571  cantnfval  9575  cantnf0  9582  cantnfres  9584  cnfcomlem  9606  hsmexlem4  10337  hsmexlem5  10338  axdc3lem2  10359  ttukeylem3  10419  hashfun  14358  s1dmALT  14531  swrdval  14565  swrd0  14580  s2dmALT  14829  s4dom  14840  dmtrclfv  14939  relexpnndm  14962  relexpdmg  14963  relexpdmd  14965  relexpnnrn  14966  relexpfld  14970  relexpaddg  14974  shftdm  14992  rlim  15416  ramval  16934  isstruct2  17074  setsvalg  17091  setsdm  17095  prdsval  17373  homfeqbas  17617  invf  17690  dfiso2  17694  oppciso  17703  cicsym  17726  sscfn1  17739  sscfn2  17740  isssc  17742  rescval  17749  rescval2  17750  issubc  17757  issubc2  17758  cofuval  17804  resfval  17814  resfval2  17815  resf1st  17816  estrreslem2  18059  prfval  18120  lubdm  18270  glbdm  18283  joindm  18294  meetdm  18308  islat  18354  isclat  18421  oduclatb  18428  gsumvalx  18599  mndpsuppss  18688  cntzrcl  19254  f1omvdco2  19375  pmtrfrn  19385  symgsssg  19394  symgfisg  19395  symggen  19397  pmtrdifwrdellem3  19410  pmtrdifwrdel2lem1  19411  pmtrdifwrdel  19412  pmtrdifwrdel2  19413  psgnunilem1  19420  psgnunilem5  19421  psgnunilem2  19422  psgnunilem3  19423  psgneldm  19430  dmdprd  19927  dprdval  19932  dpjfval  19984  ablfaclem3  20016  cofipsgn  21546  elocv  21621  ishil  21671  dsmmval  21687  mpfrcl  22038  mamudm  22337  mavmuldm  22492  mavmul0g  22495  m1detdiag  22539  decpmatval0  22706  decpmatval  22707  pmatcollpw3lem  22725  iscnp2  23181  ptval  23512  ptcmplem2  23995  cnextfval  24004  tsmsval2  24072  ustbas2  24167  utopval  24174  tusval  24207  ucnval  24218  iscfilu  24229  psmetdmdm  24247  xmetdmdm  24277  blfvalps  24325  setsmstopn  24420  tmsval  24423  metuval  24491  tngtopn  24592  cfilfval  25218  caufval  25229  limcfval  25827  dvfval  25852  dvbsss  25857  perfdvf  25858  dvmptresicc  25871  dvn2bss  25886  dvnres  25887  dvcmul  25901  dvcmulf  25902  dvcj  25908  dvnfre  25910  dvexp  25911  dvmptres3  25914  dvmptcl  25917  dvmptadd  25918  dvmptmul  25919  dvmptres2  25920  dvmptcmul  25922  dvmptcj  25926  dvmptco  25930  rolle  25948  cmvth  25949  cmvthOLD  25950  mvth  25951  dvlip  25952  dvlipcn  25953  dvlip2  25954  c1liplem1  25955  dveq0  25959  dv11cn  25960  dvle  25966  dvivthlem1  25967  dvivth  25969  dvne0  25970  lhop1lem  25972  lhop2  25974  lhop  25975  dvcnvrelem1  25976  dvcvx  25979  dvfsumle  25980  dvfsumleOLD  25981  dvfsumge  25982  dvfsumabs  25983  dvmptrecl  25984  dvfsumlem2  25987  dvfsumlem2OLD  25988  itgsubstlem  26009  taylfval  26320  tayl0  26323  dvtaylp  26332  dvntaylp  26333  dvntaylp0  26334  taylthlem1  26335  taylthlem2  26336  taylthlem2OLD  26337  ulmdvlem1  26363  pserdv  26393  pige3ALT  26483  logtayl  26623  relogbf  26755  lgamgulmlem2  26994  nosupdm  27670  nosupbday  27671  nosupres  27673  nosupbnd1lem1  27674  nosupbnd1  27680  nosupbnd2  27682  noinfdm  27685  noinfbday  27686  noinfbnd1  27695  noinfbnd2  27697  perpln1  28731  isuhgr  29082  isushgr  29083  uhgreq12g  29087  isuhgrop  29092  uhgrun  29096  uhgrstrrepe  29100  isupgr  29106  upgrop  29116  isumgr  29117  upgr1e  29135  upgrun  29140  umgrun  29142  isuspgr  29174  isusgr  29175  isuspgrop  29183  isusgrop  29184  ausgrusgrb  29187  usgrstrrepe  29257  uspgr1e  29266  issubgr  29293  uhgrspansubgrlem  29312  usgrexi  29463  vtxdgfval  29490  vtxdeqd  29500  vtxdun  29504  1loopgrvd0  29527  1hevtxdg0  29528  1hevtxdg1  29529  umgr2v2e  29548  umgr2v2evd2  29550  ewlksfval  29624  wksfval  29632  wlkres  29691  wlkp1  29702  eupths  30224  eupthres  30239  trlsegvdeglem4  30247  trlsegvdeglem5  30248  grporndm  30534  hmoval  30834  gsumhashmul  33099  symgcom2  33115  symgcntz  33116  pmtrcnel2  33121  cycpmco2f1  33155  cycpmrn  33174  tocyccntz  33175  fxpval  33196  fxpgaval  33198  1arithidomlem2  33566  1arithidom  33567  minplyval  33811  smatrcl  33902  metidval  33996  pstmval  34001  prsssdm  34023  ordtrestNEW  34027  ofcfval  34204  ofcfval3  34208  brae  34347  braew  34348  faeval  34352  mbfmcst  34365  carsgval  34409  issibf  34439  sitmval  34455  0rrv  34557  dstrvprob  34578  fineqvac  35221  satfdm  35512  fmlafv  35523  fmla  35524  fmlasuc0  35527  satfdmfmla  35543  cnndvlem2  36681  bj-finsumval0  37429  cureq  37736  curf  37738  curunc  37742  sdclem2  37882  ismtyval  37940  isass  37986  isexid  37987  ismndo2  38014  exidreslem  38017  rngodm1dm2  38072  divrngcl  38097  isdrngo2  38098  cnvref4  38482  isopos  39379  isatl  39498  dibffval  41339  dibfval  41340  conrel2d  43847  iunrelexp0  43885  dmtrclfvRP  43913  rntrclfvRP  43914  neicvgbex  44295  dvsconst  44513  expgrowth  44518  fnlimfvre  45860  dvsinax  46099  dvcosax  46112  dvbdfbdioolem1  46114  itgsinexplem1  46140  itgcoscmulx  46155  dirkeritg  46288  dirkercncflem2  46290  fourierdlem60  46352  fourierdlem61  46353  fourierdlem74  46366  fourierdlem75  46367  fourierdlem80  46372  fourierdlem94  46386  fourierdlem103  46395  fourierdlem104  46396  fourierdlem113  46405  dmvon  46792  ovnovollem1  46842  smflimlem3  46959  smflimlem4  46960  smflim  46963  smflim2  46992  smfpimcc  46994  smflimmpt  46996  smfsuplem2  46998  smfsuplem3  46999  smfsup  47000  smfsupmpt  47001  smfinflem  47003  smfinf  47004  smfinfmpt  47005  smflimsuplem1  47006  smflimsuplem2  47007  smflimsuplem3  47008  smflimsuplem4  47009  smflimsuplem7  47012  smflimsup  47014  smflimsupmpt  47015  smfliminf  47017  smfliminfmpt  47018  dfateq12d  47314  isubgruhgr  48056  grimidvtxedg  48073  ushggricedg  48115  isubgrgrim  48117  stgrusgra  48147  gpgiedgdmel  48237  gpgusgra  48245  upwlksfval  48323  dmrnxp  49024  lubeldm2d  49145  glbeldm2d  49146  glbprlem  49152  isclatd  49170  isopropdlem  49227  dmdm  49240  infsubc2  49248  infsubc2d  49249  oppfvalg  49313  reldmprcof1  49568  reldmprcof2  49569  dfinito4  49688  reldmlan2  49804  reldmran2  49805  termolmd  49857