Theorem dmeqd 5844

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-dm 5624

This theorem is referenced by:  dmxpid  5869  rneq  5875  dmxpss  6118  dmsnopss  6161  dmsnsnsn  6167  f10d  6797  fndmin  6978  fninfp  7108  fndifnfp  7110  ovmpt3rabdm  7605  elxp4  7852  1stval  7923  fo1st  7941  f1stres  7945  bropopvvv  8020  bropfvvvv  8022  mpocurryd  8199  errn  8644  xpassen  8984  xpdom2  8985  oicl  9415  oif  9416  hartogslem1  9428  cantnfdm  9554  cantnfval  9558  cantnf0  9565  cantnfres  9567  cnfcomlem  9589  hsmexlem4  10320  hsmexlem5  10321  axdc3lem2  10342  ttukeylem3  10402  hashfun  14344  s1dmALT  14517  swrdval  14551  swrd0  14566  s2dmALT  14815  s4dom  14826  dmtrclfv  14925  relexpnndm  14948  relexpdmg  14949  relexpdmd  14951  relexpnnrn  14952  relexpfld  14956  relexpaddg  14960  shftdm  14978  rlim  15402  ramval  16920  isstruct2  17060  setsvalg  17077  setsdm  17081  prdsval  17359  homfeqbas  17602  invf  17675  dfiso2  17679  oppciso  17688  cicsym  17711  sscfn1  17724  sscfn2  17725  isssc  17727  rescval  17734  rescval2  17735  issubc  17742  issubc2  17743  cofuval  17789  resfval  17799  resfval2  17800  resf1st  17801  estrreslem2  18044  prfval  18105  lubdm  18255  glbdm  18268  joindm  18279  meetdm  18293  islat  18339  isclat  18406  oduclatb  18413  gsumvalx  18584  mndpsuppss  18673  cntzrcl  19239  f1omvdco2  19360  pmtrfrn  19370  symgsssg  19379  symgfisg  19380  symggen  19382  pmtrdifwrdellem3  19395  pmtrdifwrdel2lem1  19396  pmtrdifwrdel  19397  pmtrdifwrdel2  19398  psgnunilem1  19405  psgnunilem5  19406  psgnunilem2  19407  psgnunilem3  19408  psgneldm  19415  dmdprd  19912  dprdval  19917  dpjfval  19969  ablfaclem3  20001  cofipsgn  21530  elocv  21605  ishil  21655  dsmmval  21671  mpfrcl  22020  mamudm  22310  mavmuldm  22465  mavmul0g  22468  m1detdiag  22512  decpmatval0  22679  decpmatval  22680  pmatcollpw3lem  22698  iscnp2  23154  ptval  23485  ptcmplem2  23968  cnextfval  23977  tsmsval2  24045  ustbas2  24140  utopval  24147  tusval  24180  ucnval  24191  iscfilu  24202  psmetdmdm  24220  xmetdmdm  24250  blfvalps  24298  setsmstopn  24393  tmsval  24396  metuval  24464  tngtopn  24565  cfilfval  25191  caufval  25202  limcfval  25800  dvfval  25825  dvbsss  25830  perfdvf  25831  dvmptresicc  25844  dvn2bss  25859  dvnres  25860  dvcmul  25874  dvcmulf  25875  dvcj  25881  dvnfre  25883  dvexp  25884  dvmptres3  25887  dvmptcl  25890  dvmptadd  25891  dvmptmul  25892  dvmptres2  25893  dvmptcmul  25895  dvmptcj  25899  dvmptco  25903  rolle  25921  cmvth  25922  cmvthOLD  25923  mvth  25924  dvlip  25925  dvlipcn  25926  dvlip2  25927  c1liplem1  25928  dveq0  25932  dv11cn  25933  dvle  25939  dvivthlem1  25940  dvivth  25942  dvne0  25943  lhop1lem  25945  lhop2  25947  lhop  25948  dvcnvrelem1  25949  dvcvx  25952  dvfsumle  25953  dvfsumleOLD  25954  dvfsumge  25955  dvfsumabs  25956  dvmptrecl  25957  dvfsumlem2  25960  dvfsumlem2OLD  25961  itgsubstlem  25982  taylfval  26293  tayl0  26296  dvtaylp  26305  dvntaylp  26306  dvntaylp0  26307  taylthlem1  26308  taylthlem2  26309  taylthlem2OLD  26310  ulmdvlem1  26336  pserdv  26366  pige3ALT  26456  logtayl  26596  relogbf  26728  lgamgulmlem2  26967  nosupdm  27643  nosupbday  27644  nosupres  27646  nosupbnd1lem1  27647  nosupbnd1  27653  nosupbnd2  27655  noinfdm  27658  noinfbday  27659  noinfbnd1  27668  noinfbnd2  27670  perpln1  28688  isuhgr  29038  isushgr  29039  uhgreq12g  29043  isuhgrop  29048  uhgrun  29052  uhgrstrrepe  29056  isupgr  29062  upgrop  29072  isumgr  29073  upgr1e  29091  upgrun  29096  umgrun  29098  isuspgr  29130  isusgr  29131  isuspgrop  29139  isusgrop  29140  ausgrusgrb  29143  usgrstrrepe  29213  uspgr1e  29222  issubgr  29249  uhgrspansubgrlem  29268  usgrexi  29419  vtxdgfval  29446  vtxdeqd  29456  vtxdun  29460  1loopgrvd0  29483  1hevtxdg0  29484  1hevtxdg1  29485  umgr2v2e  29504  umgr2v2evd2  29506  ewlksfval  29580  wksfval  29588  wlkres  29647  wlkp1  29658  eupths  30180  eupthres  30195  trlsegvdeglem4  30203  trlsegvdeglem5  30204  grporndm  30490  hmoval  30790  gsumhashmul  33041  symgcom2  33053  symgcntz  33054  pmtrcnel2  33059  cycpmco2f1  33093  cycpmrn  33112  tocyccntz  33113  fxpval  33134  fxpgaval  33136  1arithidomlem2  33501  1arithidom  33502  minplyval  33718  smatrcl  33809  metidval  33903  pstmval  33908  prsssdm  33930  ordtrestNEW  33934  ofcfval  34111  ofcfval3  34115  brae  34254  braew  34255  faeval  34259  mbfmcst  34272  carsgval  34316  issibf  34346  sitmval  34362  0rrv  34464  dstrvprob  34485  fineqvac  35139  satfdm  35413  fmlafv  35424  fmla  35425  fmlasuc0  35428  satfdmfmla  35444  cnndvlem2  36580  bj-finsumval0  37327  cureq  37644  curf  37646  curunc  37650  sdclem2  37790  ismtyval  37848  isass  37894  isexid  37895  ismndo2  37922  exidreslem  37925  rngodm1dm2  37980  divrngcl  38005  isdrngo2  38006  cnvref4  38386  isopos  39227  isatl  39346  dibffval  41187  dibfval  41188  conrel2d  43705  iunrelexp0  43743  dmtrclfvRP  43771  rntrclfvRP  43772  neicvgbex  44153  dvsconst  44371  expgrowth  44376  fnlimfvre  45720  dvsinax  45959  dvcosax  45972  dvbdfbdioolem1  45974  itgsinexplem1  46000  itgcoscmulx  46015  dirkeritg  46148  dirkercncflem2  46150  fourierdlem60  46212  fourierdlem61  46213  fourierdlem74  46226  fourierdlem75  46227  fourierdlem80  46232  fourierdlem94  46246  fourierdlem103  46255  fourierdlem104  46256  fourierdlem113  46265  dmvon  46652  ovnovollem1  46702  smflimlem3  46819  smflimlem4  46820  smflim  46823  smflim2  46852  smfpimcc  46854  smflimmpt  46856  smfsuplem2  46858  smfsuplem3  46859  smfsup  46860  smfsupmpt  46861  smfinflem  46863  smfinf  46864  smfinfmpt  46865  smflimsuplem1  46866  smflimsuplem2  46867  smflimsuplem3  46868  smflimsuplem4  46869  smflimsuplem7  46872  smflimsup  46874  smflimsupmpt  46875  smfliminf  46877  smfliminfmpt  46878  dfateq12d  47165  isubgruhgr  47907  grimidvtxedg  47924  ushggricedg  47966  isubgrgrim  47968  stgrusgra  47998  gpgiedgdmel  48088  gpgusgra  48096  upwlksfval  48174  dmrnxp  48876  lubeldm2d  48997  glbeldm2d  48998  glbprlem  49004  isclatd  49022  isopropdlem  49080  dmdm  49093  infsubc2  49101  infsubc2d  49102  oppfvalg  49166  reldmprcof1  49421  reldmprcof2  49422  dfinito4  49541  reldmlan2  49657  reldmran2  49658  termolmd  49710