Theorem dmeqd 5904

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-dm 5686

This theorem is referenced by:  dmxpid  5928  rneq  5934  dmxpss  6168  dmsnopss  6211  dmsnsnsn  6217  f10d  6865  fndmin  7044  fninfp  7169  fndifnfp  7171  ovmpt3rabdm  7662  elxp4  7910  1stval  7974  fo1st  7992  f1stres  7996  bropopvvv  8073  bropfvvvv  8075  mpocurryd  8251  errn  8722  xpassen  9063  xpdom2  9064  oicl  9521  oif  9522  hartogslem1  9534  cantnfdm  9656  cantnfval  9660  cantnf0  9667  cantnfres  9669  cnfcomlem  9691  hsmexlem4  10421  hsmexlem5  10422  axdc3lem2  10443  ttukeylem3  10503  hashfun  14394  s1dmALT  14556  swrdval  14590  swrd0  14605  s2dmALT  14856  s4dom  14867  dmtrclfv  14962  relexpnndm  14985  relexpdmg  14986  relexpdmd  14988  relexpnnrn  14989  relexpfld  14993  relexpaddg  14997  shftdm  15015  rlim  15436  ramval  16938  isstruct2  17079  setsvalg  17096  setsdm  17100  prdsval  17398  homfeqbas  17637  invf  17712  dfiso2  17716  oppciso  17725  cicsym  17748  sscfn1  17761  sscfn2  17762  isssc  17764  rescval  17771  rescval2  17772  issubc  17782  issubc2  17783  cofuval  17829  resfval  17839  resfval2  17840  resf1st  17841  estrreslem2  18087  prfval  18148  lubdm  18301  glbdm  18314  joindm  18325  meetdm  18339  islat  18383  isclat  18450  oduclatb  18457  gsumvalx  18592  cntzrcl  19186  f1omvdco2  19311  pmtrfrn  19321  symgsssg  19330  symgfisg  19331  symggen  19333  pmtrdifwrdellem3  19346  pmtrdifwrdel2lem1  19347  pmtrdifwrdel  19348  pmtrdifwrdel2  19349  psgnunilem1  19356  psgnunilem5  19357  psgnunilem2  19358  psgnunilem3  19359  psgneldm  19366  dmdprd  19863  dprdval  19868  dpjfval  19920  ablfaclem3  19952  cofipsgn  21138  elocv  21213  ishil  21265  dsmmval  21281  mpfrcl  21640  mamudm  21882  mavmuldm  22044  mavmul0g  22047  m1detdiag  22091  decpmatval0  22258  decpmatval  22259  pmatcollpw3lem  22277  iscnp2  22735  ptval  23066  ptcmplem2  23549  cnextfval  23558  tsmsval2  23626  ustbas2  23722  utopval  23729  tusval  23762  ucnval  23774  iscfilu  23785  psmetdmdm  23803  xmetdmdm  23833  blfvalps  23881  setsmstopn  23978  tmsval  23981  metuval  24050  tngtopn  24159  cfilfval  24773  caufval  24784  limcfval  25381  dvfval  25406  dvbsss  25411  perfdvf  25412  dvmptresicc  25425  dvn2bss  25439  dvnres  25440  dvcmul  25453  dvcmulf  25454  dvcj  25459  dvnfre  25461  dvexp  25462  dvmptres3  25465  dvmptcl  25468  dvmptadd  25469  dvmptmul  25470  dvmptres2  25471  dvmptcmul  25473  dvmptcj  25477  dvmptco  25481  rolle  25499  cmvth  25500  mvth  25501  dvlip  25502  dvlipcn  25503  dvlip2  25504  c1liplem1  25505  dveq0  25509  dv11cn  25510  dvle  25516  dvivthlem1  25517  dvivth  25519  dvne0  25520  lhop1lem  25522  lhop2  25524  lhop  25525  dvcnvrelem1  25526  dvcvx  25529  dvfsumle  25530  dvfsumge  25531  dvfsumabs  25532  dvmptrecl  25533  dvfsumlem2  25536  itgsubstlem  25557  taylfval  25863  tayl0  25866  dvtaylp  25874  dvntaylp  25875  dvntaylp0  25876  taylthlem1  25877  taylthlem2  25878  ulmdvlem1  25904  pserdv  25933  pige3ALT  26021  logtayl  26160  relogbf  26286  lgamgulmlem2  26524  nosupdm  27197  nosupbday  27198  nosupres  27200  nosupbnd1lem1  27201  nosupbnd1  27207  nosupbnd2  27209  noinfdm  27212  noinfbday  27213  noinfbnd1  27222  noinfbnd2  27224  perpln1  27951  isuhgr  28310  isushgr  28311  uhgreq12g  28315  isuhgrop  28320  uhgrun  28324  uhgrstrrepe  28328  isupgr  28334  upgrop  28344  isumgr  28345  upgr1e  28363  upgrun  28368  umgrun  28370  isuspgr  28402  isusgr  28403  isuspgrop  28411  isusgrop  28412  ausgrusgrb  28415  usgrstrrepe  28482  uspgr1e  28491  usgrexmpl  28510  issubgr  28518  uhgrspansubgrlem  28537  usgrexi  28688  vtxdgfval  28714  vtxdeqd  28724  vtxdun  28728  1loopgrvd0  28751  1hevtxdg0  28752  1hevtxdg1  28753  umgr2v2e  28772  umgr2v2evd2  28774  ewlksfval  28848  wksfval  28856  wlkres  28917  wlkp1  28928  eupths  29443  eupthres  29458  trlsegvdeglem4  29466  trlsegvdeglem5  29467  grporndm  29751  hmoval  30051  gsumhashmul  32196  symgcom2  32233  symgcntz  32234  pmtrcnel2  32239  cycpmco2f1  32271  cycpmrn  32290  tocyccntz  32291  minplyval  32755  smatrcl  32765  metidval  32859  pstmval  32864  prsssdm  32886  ordtrestNEW  32890  ofcfval  33085  ofcfval3  33089  brae  33228  braew  33229  faeval  33233  mbfmcst  33247  carsgval  33291  issibf  33321  sitmval  33337  0rrv  33439  dstrvprob  33459  fineqvac  34086  satfdm  34349  fmlafv  34360  fmla  34361  fmlasuc0  34364  satfdmfmla  34380  gg-cmvth  35170  gg-dvfsumle  35171  gg-dvfsumlem2  35172  cnndvlem2  35403  bj-finsumval0  36155  cureq  36453  curf  36455  curunc  36459  sdclem2  36599  ismtyval  36657  isass  36703  isexid  36704  ismndo2  36731  exidreslem  36734  rngodm1dm2  36789  divrngcl  36814  isdrngo2  36815  cnvref4  37208  isopos  38039  isatl  38158  dibffval  40000  dibfval  40001  conrel2d  42401  iunrelexp0  42439  dmtrclfvRP  42467  rntrclfvRP  42468  neicvgbex  42849  dvsconst  43075  expgrowth  43080  fnlimfvre  44377  dvsinax  44616  dvcosax  44629  dvbdfbdioolem1  44631  itgsinexplem1  44657  itgcoscmulx  44672  dirkeritg  44805  dirkercncflem2  44807  fourierdlem60  44869  fourierdlem61  44870  fourierdlem74  44883  fourierdlem75  44884  fourierdlem80  44889  fourierdlem94  44903  fourierdlem103  44912  fourierdlem104  44913  fourierdlem113  44922  dmvon  45309  ovnovollem1  45359  smflimlem3  45476  smflimlem4  45477  smflim  45480  smflim2  45509  smfpimcc  45511  smflimmpt  45513  smfsuplem2  45515  smfsuplem3  45516  smfsup  45517  smfsupmpt  45518  smfinflem  45520  smfinf  45521  smfinfmpt  45522  smflimsuplem1  45523  smflimsuplem2  45524  smflimsuplem3  45525  smflimsuplem4  45526  smflimsuplem7  45529  smflimsup  45531  smflimsupmpt  45532  smfliminf  45534  smfliminfmpt  45535  dfateq12d  45821  isomgr  46478  isomgreqve  46480  ushrisomgr  46496  upwlksfval  46500  mndpsuppss  47001  lubeldm2d  47545  glbeldm2d  47546  glbprlem  47552  isclatd  47562