Theorem dmeqd 5859

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-dm 5641

This theorem is referenced by:  dmxpid  5883  rneq  5889  dmxpss  6132  dmsnopss  6175  dmsnsnsn  6181  f10d  6816  fndmin  6999  fninfp  7130  fndifnfp  7132  ovmpt3rabdm  7628  elxp4  7878  1stval  7949  fo1st  7967  f1stres  7971  bropopvvv  8046  bropfvvvv  8048  mpocurryd  8225  errn  8670  xpassen  9012  xpdom2  9013  oicl  9458  oif  9459  hartogslem1  9471  cantnfdm  9593  cantnfval  9597  cantnf0  9604  cantnfres  9606  cnfcomlem  9628  hsmexlem4  10358  hsmexlem5  10359  axdc3lem2  10380  ttukeylem3  10440  hashfun  14378  s1dmALT  14550  swrdval  14584  swrd0  14599  s2dmALT  14850  s4dom  14861  dmtrclfv  14960  relexpnndm  14983  relexpdmg  14984  relexpdmd  14986  relexpnnrn  14987  relexpfld  14991  relexpaddg  14995  shftdm  15013  rlim  15437  ramval  16955  isstruct2  17095  setsvalg  17112  setsdm  17116  prdsval  17394  homfeqbas  17633  invf  17706  dfiso2  17710  oppciso  17719  cicsym  17742  sscfn1  17755  sscfn2  17756  isssc  17758  rescval  17765  rescval2  17766  issubc  17773  issubc2  17774  cofuval  17820  resfval  17830  resfval2  17831  resf1st  17832  estrreslem2  18075  prfval  18136  lubdm  18286  glbdm  18299  joindm  18310  meetdm  18324  islat  18368  isclat  18435  oduclatb  18442  gsumvalx  18579  mndpsuppss  18668  cntzrcl  19235  f1omvdco2  19354  pmtrfrn  19364  symgsssg  19373  symgfisg  19374  symggen  19376  pmtrdifwrdellem3  19389  pmtrdifwrdel2lem1  19390  pmtrdifwrdel  19391  pmtrdifwrdel2  19392  psgnunilem1  19399  psgnunilem5  19400  psgnunilem2  19401  psgnunilem3  19402  psgneldm  19409  dmdprd  19906  dprdval  19911  dpjfval  19963  ablfaclem3  19995  cofipsgn  21478  elocv  21553  ishil  21603  dsmmval  21619  mpfrcl  21968  mamudm  22258  mavmuldm  22413  mavmul0g  22416  m1detdiag  22460  decpmatval0  22627  decpmatval  22628  pmatcollpw3lem  22646  iscnp2  23102  ptval  23433  ptcmplem2  23916  cnextfval  23925  tsmsval2  23993  ustbas2  24089  utopval  24096  tusval  24129  ucnval  24140  iscfilu  24151  psmetdmdm  24169  xmetdmdm  24199  blfvalps  24247  setsmstopn  24342  tmsval  24345  metuval  24413  tngtopn  24514  cfilfval  25140  caufval  25151  limcfval  25749  dvfval  25774  dvbsss  25779  perfdvf  25780  dvmptresicc  25793  dvn2bss  25808  dvnres  25809  dvcmul  25823  dvcmulf  25824  dvcj  25830  dvnfre  25832  dvexp  25833  dvmptres3  25836  dvmptcl  25839  dvmptadd  25840  dvmptmul  25841  dvmptres2  25842  dvmptcmul  25844  dvmptcj  25848  dvmptco  25852  rolle  25870  cmvth  25871  cmvthOLD  25872  mvth  25873  dvlip  25874  dvlipcn  25875  dvlip2  25876  c1liplem1  25877  dveq0  25881  dv11cn  25882  dvle  25888  dvivthlem1  25889  dvivth  25891  dvne0  25892  lhop1lem  25894  lhop2  25896  lhop  25897  dvcnvrelem1  25898  dvcvx  25901  dvfsumle  25902  dvfsumleOLD  25903  dvfsumge  25904  dvfsumabs  25905  dvmptrecl  25906  dvfsumlem2  25909  dvfsumlem2OLD  25910  itgsubstlem  25931  taylfval  26242  tayl0  26245  dvtaylp  26254  dvntaylp  26255  dvntaylp0  26256  taylthlem1  26257  taylthlem2  26258  taylthlem2OLD  26259  ulmdvlem1  26285  pserdv  26315  pige3ALT  26405  logtayl  26545  relogbf  26677  lgamgulmlem2  26916  nosupdm  27592  nosupbday  27593  nosupres  27595  nosupbnd1lem1  27596  nosupbnd1  27602  nosupbnd2  27604  noinfdm  27607  noinfbday  27608  noinfbnd1  27617  noinfbnd2  27619  perpln1  28613  isuhgr  28963  isushgr  28964  uhgreq12g  28968  isuhgrop  28973  uhgrun  28977  uhgrstrrepe  28981  isupgr  28987  upgrop  28997  isumgr  28998  upgr1e  29016  upgrun  29021  umgrun  29023  isuspgr  29055  isusgr  29056  isuspgrop  29064  isusgrop  29065  ausgrusgrb  29068  usgrstrrepe  29138  uspgr1e  29147  issubgr  29174  uhgrspansubgrlem  29193  usgrexi  29344  vtxdgfval  29371  vtxdeqd  29381  vtxdun  29385  1loopgrvd0  29408  1hevtxdg0  29409  1hevtxdg1  29410  umgr2v2e  29429  umgr2v2evd2  29431  ewlksfval  29505  wksfval  29513  wlkres  29572  wlkp1  29583  eupths  30102  eupthres  30117  trlsegvdeglem4  30125  trlsegvdeglem5  30126  grporndm  30412  hmoval  30712  gsumhashmul  32974  symgcom2  33014  symgcntz  33015  pmtrcnel2  33020  cycpmco2f1  33054  cycpmrn  33073  tocyccntz  33074  fxpval  33095  fxpgaval  33097  1arithidomlem2  33480  1arithidom  33481  minplyval  33668  smatrcl  33759  metidval  33853  pstmval  33858  prsssdm  33880  ordtrestNEW  33884  ofcfval  34061  ofcfval3  34065  brae  34204  braew  34205  faeval  34209  mbfmcst  34223  carsgval  34267  issibf  34297  sitmval  34313  0rrv  34415  dstrvprob  34436  fineqvac  35060  satfdm  35329  fmlafv  35340  fmla  35341  fmlasuc0  35344  satfdmfmla  35360  cnndvlem2  36499  bj-finsumval0  37246  cureq  37563  curf  37565  curunc  37569  sdclem2  37709  ismtyval  37767  isass  37813  isexid  37814  ismndo2  37841  exidreslem  37844  rngodm1dm2  37899  divrngcl  37924  isdrngo2  37925  cnvref4  38305  isopos  39146  isatl  39265  dibffval  41107  dibfval  41108  conrel2d  43626  iunrelexp0  43664  dmtrclfvRP  43692  rntrclfvRP  43693  neicvgbex  44074  dvsconst  44292  expgrowth  44297  fnlimfvre  45645  dvsinax  45884  dvcosax  45897  dvbdfbdioolem1  45899  itgsinexplem1  45925  itgcoscmulx  45940  dirkeritg  46073  dirkercncflem2  46075  fourierdlem60  46137  fourierdlem61  46138  fourierdlem74  46151  fourierdlem75  46152  fourierdlem80  46157  fourierdlem94  46171  fourierdlem103  46180  fourierdlem104  46181  fourierdlem113  46190  dmvon  46577  ovnovollem1  46627  smflimlem3  46744  smflimlem4  46745  smflim  46748  smflim2  46777  smfpimcc  46779  smflimmpt  46781  smfsuplem2  46783  smfsuplem3  46784  smfsup  46785  smfsupmpt  46786  smfinflem  46788  smfinf  46789  smfinfmpt  46790  smflimsuplem1  46791  smflimsuplem2  46792  smflimsuplem3  46793  smflimsuplem4  46794  smflimsuplem7  46797  smflimsup  46799  smflimsupmpt  46800  smfliminf  46802  smfliminfmpt  46803  dfateq12d  47100  isubgruhgr  47841  grimidvtxedg  47858  ushggricedg  47900  isubgrgrim  47902  stgrusgra  47931  gpgiedgdmel  48013  gpgusgra  48021  upwlksfval  48096  dmrnxp  48798  lubeldm2d  48919  glbeldm2d  48920  glbprlem  48926  isclatd  48944  isopropdlem  49002  dmdm  49015  infsubc2  49023  infsubc2d  49024  oppfvalg  49088  reldmprcof1  49343  reldmprcof2  49344  dfinito4  49463  reldmlan2  49579  reldmran2  49580  termolmd  49632