Theorem dmeqd 5872

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-dm 5651

This theorem is referenced by:  dmxpid  5897  rneq  5903  dmxpss  6147  dmsnopss  6190  dmsnsnsn  6196  f10d  6837  fndmin  7020  fninfp  7151  fndifnfp  7153  ovmpt3rabdm  7651  elxp4  7901  1stval  7973  fo1st  7991  f1stres  7995  bropopvvv  8072  bropfvvvv  8074  mpocurryd  8251  errn  8696  xpassen  9040  xpdom2  9041  oicl  9489  oif  9490  hartogslem1  9502  cantnfdm  9624  cantnfval  9628  cantnf0  9635  cantnfres  9637  cnfcomlem  9659  hsmexlem4  10389  hsmexlem5  10390  axdc3lem2  10411  ttukeylem3  10471  hashfun  14409  s1dmALT  14581  swrdval  14615  swrd0  14630  s2dmALT  14881  s4dom  14892  dmtrclfv  14991  relexpnndm  15014  relexpdmg  15015  relexpdmd  15017  relexpnnrn  15018  relexpfld  15022  relexpaddg  15026  shftdm  15044  rlim  15468  ramval  16986  isstruct2  17126  setsvalg  17143  setsdm  17147  prdsval  17425  homfeqbas  17664  invf  17737  dfiso2  17741  oppciso  17750  cicsym  17773  sscfn1  17786  sscfn2  17787  isssc  17789  rescval  17796  rescval2  17797  issubc  17804  issubc2  17805  cofuval  17851  resfval  17861  resfval2  17862  resf1st  17863  estrreslem2  18106  prfval  18167  lubdm  18317  glbdm  18330  joindm  18341  meetdm  18355  islat  18399  isclat  18466  oduclatb  18473  gsumvalx  18610  mndpsuppss  18699  cntzrcl  19266  f1omvdco2  19385  pmtrfrn  19395  symgsssg  19404  symgfisg  19405  symggen  19407  pmtrdifwrdellem3  19420  pmtrdifwrdel2lem1  19421  pmtrdifwrdel  19422  pmtrdifwrdel2  19423  psgnunilem1  19430  psgnunilem5  19431  psgnunilem2  19432  psgnunilem3  19433  psgneldm  19440  dmdprd  19937  dprdval  19942  dpjfval  19994  ablfaclem3  20026  cofipsgn  21509  elocv  21584  ishil  21634  dsmmval  21650  mpfrcl  21999  mamudm  22289  mavmuldm  22444  mavmul0g  22447  m1detdiag  22491  decpmatval0  22658  decpmatval  22659  pmatcollpw3lem  22677  iscnp2  23133  ptval  23464  ptcmplem2  23947  cnextfval  23956  tsmsval2  24024  ustbas2  24120  utopval  24127  tusval  24160  ucnval  24171  iscfilu  24182  psmetdmdm  24200  xmetdmdm  24230  blfvalps  24278  setsmstopn  24373  tmsval  24376  metuval  24444  tngtopn  24545  cfilfval  25171  caufval  25182  limcfval  25780  dvfval  25805  dvbsss  25810  perfdvf  25811  dvmptresicc  25824  dvn2bss  25839  dvnres  25840  dvcmul  25854  dvcmulf  25855  dvcj  25861  dvnfre  25863  dvexp  25864  dvmptres3  25867  dvmptcl  25870  dvmptadd  25871  dvmptmul  25872  dvmptres2  25873  dvmptcmul  25875  dvmptcj  25879  dvmptco  25883  rolle  25901  cmvth  25902  cmvthOLD  25903  mvth  25904  dvlip  25905  dvlipcn  25906  dvlip2  25907  c1liplem1  25908  dveq0  25912  dv11cn  25913  dvle  25919  dvivthlem1  25920  dvivth  25922  dvne0  25923  lhop1lem  25925  lhop2  25927  lhop  25928  dvcnvrelem1  25929  dvcvx  25932  dvfsumle  25933  dvfsumleOLD  25934  dvfsumge  25935  dvfsumabs  25936  dvmptrecl  25937  dvfsumlem2  25940  dvfsumlem2OLD  25941  itgsubstlem  25962  taylfval  26273  tayl0  26276  dvtaylp  26285  dvntaylp  26286  dvntaylp0  26287  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmdvlem1  26316  pserdv  26346  pige3ALT  26436  logtayl  26576  relogbf  26708  lgamgulmlem2  26947  nosupdm  27623  nosupbday  27624  nosupres  27626  nosupbnd1lem1  27627  nosupbnd1  27633  nosupbnd2  27635  noinfdm  27638  noinfbday  27639  noinfbnd1  27648  noinfbnd2  27650  perpln1  28644  isuhgr  28994  isushgr  28995  uhgreq12g  28999  isuhgrop  29004  uhgrun  29008  uhgrstrrepe  29012  isupgr  29018  upgrop  29028  isumgr  29029  upgr1e  29047  upgrun  29052  umgrun  29054  isuspgr  29086  isusgr  29087  isuspgrop  29095  isusgrop  29096  ausgrusgrb  29099  usgrstrrepe  29169  uspgr1e  29178  issubgr  29205  uhgrspansubgrlem  29224  usgrexi  29375  vtxdgfval  29402  vtxdeqd  29412  vtxdun  29416  1loopgrvd0  29439  1hevtxdg0  29440  1hevtxdg1  29441  umgr2v2e  29460  umgr2v2evd2  29462  ewlksfval  29536  wksfval  29544  wlkres  29605  wlkp1  29616  eupths  30136  eupthres  30151  trlsegvdeglem4  30159  trlsegvdeglem5  30160  grporndm  30446  hmoval  30746  gsumhashmul  33008  symgcom2  33048  symgcntz  33049  pmtrcnel2  33054  cycpmco2f1  33088  cycpmrn  33107  tocyccntz  33108  fxpval  33129  fxpgaval  33131  1arithidomlem2  33514  1arithidom  33515  minplyval  33702  smatrcl  33793  metidval  33887  pstmval  33892  prsssdm  33914  ordtrestNEW  33918  ofcfval  34095  ofcfval3  34099  brae  34238  braew  34239  faeval  34243  mbfmcst  34257  carsgval  34301  issibf  34331  sitmval  34347  0rrv  34449  dstrvprob  34470  fineqvac  35094  satfdm  35363  fmlafv  35374  fmla  35375  fmlasuc0  35378  satfdmfmla  35394  cnndvlem2  36533  bj-finsumval0  37280  cureq  37597  curf  37599  curunc  37603  sdclem2  37743  ismtyval  37801  isass  37847  isexid  37848  ismndo2  37875  exidreslem  37878  rngodm1dm2  37933  divrngcl  37958  isdrngo2  37959  cnvref4  38339  isopos  39180  isatl  39299  dibffval  41141  dibfval  41142  conrel2d  43660  iunrelexp0  43698  dmtrclfvRP  43726  rntrclfvRP  43727  neicvgbex  44108  dvsconst  44326  expgrowth  44331  fnlimfvre  45679  dvsinax  45918  dvcosax  45931  dvbdfbdioolem1  45933  itgsinexplem1  45959  itgcoscmulx  45974  dirkeritg  46107  dirkercncflem2  46109  fourierdlem60  46171  fourierdlem61  46172  fourierdlem74  46185  fourierdlem75  46186  fourierdlem80  46191  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  fourierdlem113  46224  dmvon  46611  ovnovollem1  46661  smflimlem3  46778  smflimlem4  46779  smflim  46782  smflim2  46811  smfpimcc  46813  smflimmpt  46815  smfsuplem2  46817  smfsuplem3  46818  smfsup  46819  smfsupmpt  46820  smfinflem  46822  smfinf  46823  smfinfmpt  46824  smflimsuplem1  46825  smflimsuplem2  46826  smflimsuplem3  46827  smflimsuplem4  46828  smflimsuplem7  46831  smflimsup  46833  smflimsupmpt  46834  smfliminf  46836  smfliminfmpt  46837  dfateq12d  47131  isubgruhgr  47872  grimidvtxedg  47889  ushggricedg  47931  isubgrgrim  47933  stgrusgra  47962  gpgiedgdmel  48044  gpgusgra  48052  upwlksfval  48127  dmrnxp  48829  lubeldm2d  48950  glbeldm2d  48951  glbprlem  48957  isclatd  48975  isopropdlem  49033  dmdm  49046  infsubc2  49054  infsubc2d  49055  oppfvalg  49119  reldmprcof1  49374  reldmprcof2  49375  dfinito4  49494  reldmlan2  49610  reldmran2  49611  termolmd  49663