Theorem dmeqd 5862

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-dm 5642

This theorem is referenced by:  dmxpid  5887  rneq  5893  dmxpss  6137  dmsnopss  6180  dmsnsnsn  6186  f10d  6816  fndmin  6999  fninfp  7130  fndifnfp  7132  ovmpt3rabdm  7627  elxp4  7874  1stval  7945  fo1st  7963  f1stres  7967  bropopvvv  8042  bropfvvvv  8044  mpocurryd  8221  errn  8668  xpassen  9011  xpdom2  9012  oicl  9446  oif  9447  hartogslem1  9459  cantnfdm  9585  cantnfval  9589  cantnf0  9596  cantnfres  9598  cnfcomlem  9620  hsmexlem4  10351  hsmexlem5  10352  axdc3lem2  10373  ttukeylem3  10433  hashfun  14372  s1dmALT  14545  swrdval  14579  swrd0  14594  s2dmALT  14843  s4dom  14854  dmtrclfv  14953  relexpnndm  14976  relexpdmg  14977  relexpdmd  14979  relexpnnrn  14980  relexpfld  14984  relexpaddg  14988  shftdm  15006  rlim  15430  ramval  16948  isstruct2  17088  setsvalg  17105  setsdm  17109  prdsval  17387  homfeqbas  17631  invf  17704  dfiso2  17708  oppciso  17717  cicsym  17740  sscfn1  17753  sscfn2  17754  isssc  17756  rescval  17763  rescval2  17764  issubc  17771  issubc2  17772  cofuval  17818  resfval  17828  resfval2  17829  resf1st  17830  estrreslem2  18073  prfval  18134  lubdm  18284  glbdm  18297  joindm  18308  meetdm  18322  islat  18368  isclat  18435  oduclatb  18442  gsumvalx  18613  mndpsuppss  18702  cntzrcl  19268  f1omvdco2  19389  pmtrfrn  19399  symgsssg  19408  symgfisg  19409  symggen  19411  pmtrdifwrdellem3  19424  pmtrdifwrdel2lem1  19425  pmtrdifwrdel  19426  pmtrdifwrdel2  19427  psgnunilem1  19434  psgnunilem5  19435  psgnunilem2  19436  psgnunilem3  19437  psgneldm  19444  dmdprd  19941  dprdval  19946  dpjfval  19998  ablfaclem3  20030  cofipsgn  21560  elocv  21635  ishil  21685  dsmmval  21701  mpfrcl  22052  mamudm  22351  mavmuldm  22506  mavmul0g  22509  m1detdiag  22553  decpmatval0  22720  decpmatval  22721  pmatcollpw3lem  22739  iscnp2  23195  ptval  23526  ptcmplem2  24009  cnextfval  24018  tsmsval2  24086  ustbas2  24181  utopval  24188  tusval  24221  ucnval  24232  iscfilu  24243  psmetdmdm  24261  xmetdmdm  24291  blfvalps  24339  setsmstopn  24434  tmsval  24437  metuval  24505  tngtopn  24606  cfilfval  25232  caufval  25243  limcfval  25841  dvfval  25866  dvbsss  25871  perfdvf  25872  dvmptresicc  25885  dvn2bss  25900  dvnres  25901  dvcmul  25915  dvcmulf  25916  dvcj  25922  dvnfre  25924  dvexp  25925  dvmptres3  25928  dvmptcl  25931  dvmptadd  25932  dvmptmul  25933  dvmptres2  25934  dvmptcmul  25936  dvmptcj  25940  dvmptco  25944  rolle  25962  cmvth  25963  cmvthOLD  25964  mvth  25965  dvlip  25966  dvlipcn  25967  dvlip2  25968  c1liplem1  25969  dveq0  25973  dv11cn  25974  dvle  25980  dvivthlem1  25981  dvivth  25983  dvne0  25984  lhop1lem  25986  lhop2  25988  lhop  25989  dvcnvrelem1  25990  dvcvx  25993  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvfsumabs  25997  dvmptrecl  25998  dvfsumlem2  26001  dvfsumlem2OLD  26002  itgsubstlem  26023  taylfval  26334  tayl0  26337  dvtaylp  26346  dvntaylp  26347  dvntaylp0  26348  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmdvlem1  26377  pserdv  26407  pige3ALT  26497  logtayl  26637  relogbf  26769  lgamgulmlem2  27008  nosupdm  27684  nosupbday  27685  nosupres  27687  nosupbnd1lem1  27688  nosupbnd1  27694  nosupbnd2  27696  noinfdm  27699  noinfbday  27700  noinfbnd1  27709  noinfbnd2  27711  perpln1  28794  isuhgr  29145  isushgr  29146  uhgreq12g  29150  isuhgrop  29155  uhgrun  29159  uhgrstrrepe  29163  isupgr  29169  upgrop  29179  isumgr  29180  upgr1e  29198  upgrun  29203  umgrun  29205  isuspgr  29237  isusgr  29238  isuspgrop  29246  isusgrop  29247  ausgrusgrb  29250  usgrstrrepe  29320  uspgr1e  29329  issubgr  29356  uhgrspansubgrlem  29375  usgrexi  29526  vtxdgfval  29553  vtxdeqd  29563  vtxdun  29567  1loopgrvd0  29590  1hevtxdg0  29591  1hevtxdg1  29592  umgr2v2e  29611  umgr2v2evd2  29613  ewlksfval  29687  wksfval  29695  wlkres  29754  wlkp1  29765  eupths  30287  eupthres  30302  trlsegvdeglem4  30310  trlsegvdeglem5  30311  grporndm  30598  hmoval  30898  gsumhashmul  33161  symgcom2  33178  symgcntz  33179  pmtrcnel2  33184  cycpmco2f1  33218  cycpmrn  33237  tocyccntz  33238  fxpval  33259  fxpgaval  33261  1arithidomlem2  33629  1arithidom  33630  minplyval  33883  smatrcl  33974  metidval  34068  pstmval  34073  prsssdm  34095  ordtrestNEW  34099  ofcfval  34276  ofcfval3  34280  brae  34419  braew  34420  faeval  34424  mbfmcst  34437  carsgval  34481  issibf  34511  sitmval  34527  0rrv  34629  dstrvprob  34650  fineqvac  35294  satfdm  35585  fmlafv  35596  fmla  35597  fmlasuc0  35600  satfdmfmla  35616  cnndvlem2  36760  bj-finsumval0  37540  cureq  37847  curf  37849  curunc  37853  sdclem2  37993  ismtyval  38051  isass  38097  isexid  38098  ismndo2  38125  exidreslem  38128  rngodm1dm2  38183  divrngcl  38208  isdrngo2  38209  cnvref4  38601  isopos  39556  isatl  39675  dibffval  41516  dibfval  41517  conrel2d  44020  iunrelexp0  44058  dmtrclfvRP  44086  rntrclfvRP  44087  neicvgbex  44468  dvsconst  44686  expgrowth  44691  fnlimfvre  46032  dvsinax  46271  dvcosax  46284  dvbdfbdioolem1  46286  itgsinexplem1  46312  itgcoscmulx  46327  dirkeritg  46460  dirkercncflem2  46462  fourierdlem60  46524  fourierdlem61  46525  fourierdlem74  46538  fourierdlem75  46539  fourierdlem80  46544  fourierdlem94  46558  fourierdlem103  46567  fourierdlem104  46568  fourierdlem113  46577  dmvon  46964  ovnovollem1  47014  smflimlem3  47131  smflimlem4  47132  smflim  47135  smflim2  47164  smfpimcc  47166  smflimmpt  47168  smfsuplem2  47170  smfsuplem3  47171  smfsup  47172  smfsupmpt  47173  smfinflem  47175  smfinf  47176  smfinfmpt  47177  smflimsuplem1  47178  smflimsuplem2  47179  smflimsuplem3  47180  smflimsuplem4  47181  smflimsuplem7  47184  smflimsup  47186  smflimsupmpt  47187  smfliminf  47189  smfliminfmpt  47190  dfateq12d  47486  isubgruhgr  48228  grimidvtxedg  48245  ushggricedg  48287  isubgrgrim  48289  stgrusgra  48319  gpgiedgdmel  48409  gpgusgra  48417  upwlksfval  48495  dmrnxp  49196  lubeldm2d  49317  glbeldm2d  49318  glbprlem  49324  isclatd  49342  isopropdlem  49399  dmdm  49412  infsubc2  49420  infsubc2d  49421  oppfvalg  49485  reldmprcof1  49740  reldmprcof2  49741  dfinito4  49860  reldmlan2  49976  reldmran2  49977  termolmd  50029