Theorem dmeqd 5930

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

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-dm 5710

This theorem is referenced by:  dmxpid  5955  rneq  5961  dmxpss  6202  dmsnopss  6245  dmsnsnsn  6251  f10d  6896  fndmin  7078  fninfp  7208  fndifnfp  7210  ovmpt3rabdm  7709  elxp4  7962  1stval  8032  fo1st  8050  f1stres  8054  bropopvvv  8131  bropfvvvv  8133  mpocurryd  8310  errn  8785  xpassen  9132  xpdom2  9133  oicl  9598  oif  9599  hartogslem1  9611  cantnfdm  9733  cantnfval  9737  cantnf0  9744  cantnfres  9746  cnfcomlem  9768  hsmexlem4  10498  hsmexlem5  10499  axdc3lem2  10520  ttukeylem3  10580  hashfun  14486  s1dmALT  14657  swrdval  14691  swrd0  14706  s2dmALT  14957  s4dom  14968  dmtrclfv  15067  relexpnndm  15090  relexpdmg  15091  relexpdmd  15093  relexpnnrn  15094  relexpfld  15098  relexpaddg  15102  shftdm  15120  rlim  15541  ramval  17055  isstruct2  17196  setsvalg  17213  setsdm  17217  prdsval  17515  homfeqbas  17754  invf  17829  dfiso2  17833  oppciso  17842  cicsym  17865  sscfn1  17878  sscfn2  17879  isssc  17881  rescval  17888  rescval2  17889  issubc  17899  issubc2  17900  cofuval  17946  resfval  17956  resfval2  17957  resf1st  17958  estrreslem2  18207  prfval  18268  lubdm  18421  glbdm  18434  joindm  18445  meetdm  18459  islat  18503  isclat  18570  oduclatb  18577  gsumvalx  18714  cntzrcl  19367  f1omvdco2  19490  pmtrfrn  19500  symgsssg  19509  symgfisg  19510  symggen  19512  pmtrdifwrdellem3  19525  pmtrdifwrdel2lem1  19526  pmtrdifwrdel  19527  pmtrdifwrdel2  19528  psgnunilem1  19535  psgnunilem5  19536  psgnunilem2  19537  psgnunilem3  19538  psgneldm  19545  dmdprd  20042  dprdval  20047  dpjfval  20099  ablfaclem3  20131  cofipsgn  21634  elocv  21709  ishil  21761  dsmmval  21777  mpfrcl  22132  mamudm  22420  mavmuldm  22577  mavmul0g  22580  m1detdiag  22624  decpmatval0  22791  decpmatval  22792  pmatcollpw3lem  22810  iscnp2  23268  ptval  23599  ptcmplem2  24082  cnextfval  24091  tsmsval2  24159  ustbas2  24255  utopval  24262  tusval  24295  ucnval  24307  iscfilu  24318  psmetdmdm  24336  xmetdmdm  24366  blfvalps  24414  setsmstopn  24511  tmsval  24514  metuval  24583  tngtopn  24692  cfilfval  25317  caufval  25328  limcfval  25927  dvfval  25952  dvbsss  25957  perfdvf  25958  dvmptresicc  25971  dvn2bss  25986  dvnres  25987  dvcmul  26001  dvcmulf  26002  dvcj  26008  dvnfre  26010  dvexp  26011  dvmptres3  26014  dvmptcl  26017  dvmptadd  26018  dvmptmul  26019  dvmptres2  26020  dvmptcmul  26022  dvmptcj  26026  dvmptco  26030  rolle  26048  cmvth  26049  cmvthOLD  26050  mvth  26051  dvlip  26052  dvlipcn  26053  dvlip2  26054  c1liplem1  26055  dveq0  26059  dv11cn  26060  dvle  26066  dvivthlem1  26067  dvivth  26069  dvne0  26070  lhop1lem  26072  lhop2  26074  lhop  26075  dvcnvrelem1  26076  dvcvx  26079  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  dvmptrecl  26084  dvfsumlem2  26087  dvfsumlem2OLD  26088  itgsubstlem  26109  taylfval  26418  tayl0  26421  dvtaylp  26430  dvntaylp  26431  dvntaylp0  26432  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmdvlem1  26461  pserdv  26491  pige3ALT  26580  logtayl  26720  relogbf  26852  lgamgulmlem2  27091  nosupdm  27767  nosupbday  27768  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1  27777  nosupbnd2  27779  noinfdm  27782  noinfbday  27783  noinfbnd1  27792  noinfbnd2  27794  perpln1  28736  isuhgr  29095  isushgr  29096  uhgreq12g  29100  isuhgrop  29105  uhgrun  29109  uhgrstrrepe  29113  isupgr  29119  upgrop  29129  isumgr  29130  upgr1e  29148  upgrun  29153  umgrun  29155  isuspgr  29187  isusgr  29188  isuspgrop  29196  isusgrop  29197  ausgrusgrb  29200  usgrstrrepe  29270  uspgr1e  29279  issubgr  29306  uhgrspansubgrlem  29325  usgrexi  29476  vtxdgfval  29503  vtxdeqd  29513  vtxdun  29517  1loopgrvd0  29540  1hevtxdg0  29541  1hevtxdg1  29542  umgr2v2e  29561  umgr2v2evd2  29563  ewlksfval  29637  wksfval  29645  wlkres  29706  wlkp1  29717  eupths  30232  eupthres  30247  trlsegvdeglem4  30255  trlsegvdeglem5  30256  grporndm  30542  hmoval  30842  gsumhashmul  33040  symgcom2  33077  symgcntz  33078  pmtrcnel2  33083  cycpmco2f1  33117  cycpmrn  33136  tocyccntz  33137  1arithidomlem2  33529  1arithidom  33530  minplyval  33698  smatrcl  33742  metidval  33836  pstmval  33841  prsssdm  33863  ordtrestNEW  33867  ofcfval  34062  ofcfval3  34066  brae  34205  braew  34206  faeval  34210  mbfmcst  34224  carsgval  34268  issibf  34298  sitmval  34314  0rrv  34416  dstrvprob  34436  fineqvac  35073  satfdm  35337  fmlafv  35348  fmla  35349  fmlasuc0  35352  satfdmfmla  35368  cnndvlem2  36504  bj-finsumval0  37251  cureq  37556  curf  37558  curunc  37562  sdclem2  37702  ismtyval  37760  isass  37806  isexid  37807  ismndo2  37834  exidreslem  37837  rngodm1dm2  37892  divrngcl  37917  isdrngo2  37918  cnvref4  38306  isopos  39136  isatl  39255  dibffval  41097  dibfval  41098  conrel2d  43626  iunrelexp0  43664  dmtrclfvRP  43692  rntrclfvRP  43693  neicvgbex  44074  dvsconst  44299  expgrowth  44304  fnlimfvre  45595  dvsinax  45834  dvcosax  45847  dvbdfbdioolem1  45849  itgsinexplem1  45875  itgcoscmulx  45890  dirkeritg  46023  dirkercncflem2  46025  fourierdlem60  46087  fourierdlem61  46088  fourierdlem74  46101  fourierdlem75  46102  fourierdlem80  46107  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  fourierdlem113  46140  dmvon  46527  ovnovollem1  46577  smflimlem3  46694  smflimlem4  46695  smflim  46698  smflim2  46727  smfpimcc  46729  smflimmpt  46731  smfsuplem2  46733  smfsuplem3  46734  smfsup  46735  smfsupmpt  46736  smfinflem  46738  smfinf  46739  smfinfmpt  46740  smflimsuplem1  46741  smflimsuplem2  46742  smflimsuplem3  46743  smflimsuplem4  46744  smflimsuplem7  46747  smflimsup  46749  smflimsupmpt  46750  smfliminf  46752  smfliminfmpt  46753  dfateq12d  47041  isubgruhgr  47738  grimidvtxedg  47760  ushggricedg  47780  isubgrgrim  47781  upwlksfval  47858  mndpsuppss  48096  lubeldm2d  48638  glbeldm2d  48639  glbprlem  48645  isclatd  48655