Theorem dmeqd 5854

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-dm 5634

This theorem is referenced by:  dmxpid  5879  rneq  5885  dmxpss  6129  dmsnopss  6172  dmsnsnsn  6178  f10d  6808  fndmin  6990  fninfp  7120  fndifnfp  7122  ovmpt3rabdm  7617  elxp4  7864  1stval  7935  fo1st  7953  f1stres  7957  bropopvvv  8032  bropfvvvv  8034  mpocurryd  8211  errn  8657  xpassen  8999  xpdom2  9000  oicl  9434  oif  9435  hartogslem1  9447  cantnfdm  9573  cantnfval  9577  cantnf0  9584  cantnfres  9586  cnfcomlem  9608  hsmexlem4  10339  hsmexlem5  10340  axdc3lem2  10361  ttukeylem3  10421  hashfun  14360  s1dmALT  14533  swrdval  14567  swrd0  14582  s2dmALT  14831  s4dom  14842  dmtrclfv  14941  relexpnndm  14964  relexpdmg  14965  relexpdmd  14967  relexpnnrn  14968  relexpfld  14972  relexpaddg  14976  shftdm  14994  rlim  15418  ramval  16936  isstruct2  17076  setsvalg  17093  setsdm  17097  prdsval  17375  homfeqbas  17619  invf  17692  dfiso2  17696  oppciso  17705  cicsym  17728  sscfn1  17741  sscfn2  17742  isssc  17744  rescval  17751  rescval2  17752  issubc  17759  issubc2  17760  cofuval  17806  resfval  17816  resfval2  17817  resf1st  17818  estrreslem2  18061  prfval  18122  lubdm  18272  glbdm  18285  joindm  18296  meetdm  18310  islat  18356  isclat  18423  oduclatb  18430  gsumvalx  18601  mndpsuppss  18690  cntzrcl  19256  f1omvdco2  19377  pmtrfrn  19387  symgsssg  19396  symgfisg  19397  symggen  19399  pmtrdifwrdellem3  19412  pmtrdifwrdel2lem1  19413  pmtrdifwrdel  19414  pmtrdifwrdel2  19415  psgnunilem1  19422  psgnunilem5  19423  psgnunilem2  19424  psgnunilem3  19425  psgneldm  19432  dmdprd  19929  dprdval  19934  dpjfval  19986  ablfaclem3  20018  cofipsgn  21548  elocv  21623  ishil  21673  dsmmval  21689  mpfrcl  22040  mamudm  22339  mavmuldm  22494  mavmul0g  22497  m1detdiag  22541  decpmatval0  22708  decpmatval  22709  pmatcollpw3lem  22727  iscnp2  23183  ptval  23514  ptcmplem2  23997  cnextfval  24006  tsmsval2  24074  ustbas2  24169  utopval  24176  tusval  24209  ucnval  24220  iscfilu  24231  psmetdmdm  24249  xmetdmdm  24279  blfvalps  24327  setsmstopn  24422  tmsval  24425  metuval  24493  tngtopn  24594  cfilfval  25220  caufval  25231  limcfval  25829  dvfval  25854  dvbsss  25859  perfdvf  25860  dvmptresicc  25873  dvn2bss  25888  dvnres  25889  dvcmul  25903  dvcmulf  25904  dvcj  25910  dvnfre  25912  dvexp  25913  dvmptres3  25916  dvmptcl  25919  dvmptadd  25920  dvmptmul  25921  dvmptres2  25922  dvmptcmul  25924  dvmptcj  25928  dvmptco  25932  rolle  25950  cmvth  25951  cmvthOLD  25952  mvth  25953  dvlip  25954  dvlipcn  25955  dvlip2  25956  c1liplem1  25957  dveq0  25961  dv11cn  25962  dvle  25968  dvivthlem1  25969  dvivth  25971  dvne0  25972  lhop1lem  25974  lhop2  25976  lhop  25977  dvcnvrelem1  25978  dvcvx  25981  dvfsumle  25982  dvfsumleOLD  25983  dvfsumge  25984  dvfsumabs  25985  dvmptrecl  25986  dvfsumlem2  25989  dvfsumlem2OLD  25990  itgsubstlem  26011  taylfval  26322  tayl0  26325  dvtaylp  26334  dvntaylp  26335  dvntaylp0  26336  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  ulmdvlem1  26365  pserdv  26395  pige3ALT  26485  logtayl  26625  relogbf  26757  lgamgulmlem2  26996  nosupdm  27672  nosupbday  27673  nosupres  27675  nosupbnd1lem1  27676  nosupbnd1  27682  nosupbnd2  27684  noinfdm  27687  noinfbday  27688  noinfbnd1  27697  noinfbnd2  27699  perpln1  28782  isuhgr  29133  isushgr  29134  uhgreq12g  29138  isuhgrop  29143  uhgrun  29147  uhgrstrrepe  29151  isupgr  29157  upgrop  29167  isumgr  29168  upgr1e  29186  upgrun  29191  umgrun  29193  isuspgr  29225  isusgr  29226  isuspgrop  29234  isusgrop  29235  ausgrusgrb  29238  usgrstrrepe  29308  uspgr1e  29317  issubgr  29344  uhgrspansubgrlem  29363  usgrexi  29514  vtxdgfval  29541  vtxdeqd  29551  vtxdun  29555  1loopgrvd0  29578  1hevtxdg0  29579  1hevtxdg1  29580  umgr2v2e  29599  umgr2v2evd2  29601  ewlksfval  29675  wksfval  29683  wlkres  29742  wlkp1  29753  eupths  30275  eupthres  30290  trlsegvdeglem4  30298  trlsegvdeglem5  30299  grporndm  30585  hmoval  30885  gsumhashmul  33150  symgcom2  33166  symgcntz  33167  pmtrcnel2  33172  cycpmco2f1  33206  cycpmrn  33225  tocyccntz  33226  fxpval  33247  fxpgaval  33249  1arithidomlem2  33617  1arithidom  33618  minplyval  33862  smatrcl  33953  metidval  34047  pstmval  34052  prsssdm  34074  ordtrestNEW  34078  ofcfval  34255  ofcfval3  34259  brae  34398  braew  34399  faeval  34403  mbfmcst  34416  carsgval  34460  issibf  34490  sitmval  34506  0rrv  34608  dstrvprob  34629  fineqvac  35272  satfdm  35563  fmlafv  35574  fmla  35575  fmlasuc0  35578  satfdmfmla  35594  cnndvlem2  36738  bj-finsumval0  37490  cureq  37797  curf  37799  curunc  37803  sdclem2  37943  ismtyval  38001  isass  38047  isexid  38048  ismndo2  38075  exidreslem  38078  rngodm1dm2  38133  divrngcl  38158  isdrngo2  38159  cnvref4  38543  isopos  39440  isatl  39559  dibffval  41400  dibfval  41401  conrel2d  43905  iunrelexp0  43943  dmtrclfvRP  43971  rntrclfvRP  43972  neicvgbex  44353  dvsconst  44571  expgrowth  44576  fnlimfvre  45918  dvsinax  46157  dvcosax  46170  dvbdfbdioolem1  46172  itgsinexplem1  46198  itgcoscmulx  46213  dirkeritg  46346  dirkercncflem2  46348  fourierdlem60  46410  fourierdlem61  46411  fourierdlem74  46424  fourierdlem75  46425  fourierdlem80  46430  fourierdlem94  46444  fourierdlem103  46453  fourierdlem104  46454  fourierdlem113  46463  dmvon  46850  ovnovollem1  46900  smflimlem3  47017  smflimlem4  47018  smflim  47021  smflim2  47050  smfpimcc  47052  smflimmpt  47054  smfsuplem2  47056  smfsuplem3  47057  smfsup  47058  smfsupmpt  47059  smfinflem  47061  smfinf  47062  smfinfmpt  47063  smflimsuplem1  47064  smflimsuplem2  47065  smflimsuplem3  47066  smflimsuplem4  47067  smflimsuplem7  47070  smflimsup  47072  smflimsupmpt  47073  smfliminf  47075  smfliminfmpt  47076  dfateq12d  47372  isubgruhgr  48114  grimidvtxedg  48131  ushggricedg  48173  isubgrgrim  48175  stgrusgra  48205  gpgiedgdmel  48295  gpgusgra  48303  upwlksfval  48381  dmrnxp  49082  lubeldm2d  49203  glbeldm2d  49204  glbprlem  49210  isclatd  49228  isopropdlem  49285  dmdm  49298  infsubc2  49306  infsubc2d  49307  oppfvalg  49371  reldmprcof1  49626  reldmprcof2  49627  dfinito4  49746  reldmlan2  49862  reldmran2  49863  termolmd  49915