Theorem dmeqd 5855

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

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

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-dm 5635

This theorem is referenced by:  dmxpid  5880  rneq  5886  dmxpss  6130  dmsnopss  6173  dmsnsnsn  6179  f10d  6809  fndmin  6992  fninfp  7123  fndifnfp  7125  ovmpt3rabdm  7620  elxp4  7867  1stval  7938  fo1st  7956  f1stres  7960  bropopvvv  8034  bropfvvvv  8036  mpocurryd  8213  errn  8660  xpassen  9003  xpdom2  9004  oicl  9438  oif  9439  hartogslem1  9451  cantnfdm  9579  cantnfval  9583  cantnf0  9590  cantnfres  9592  cnfcomlem  9614  hsmexlem4  10345  hsmexlem5  10346  axdc3lem2  10367  ttukeylem3  10427  hashfun  14393  s1dmALT  14566  swrdval  14600  swrd0  14615  s2dmALT  14864  s4dom  14875  dmtrclfv  14974  relexpnndm  14997  relexpdmg  14998  relexpdmd  15000  relexpnnrn  15001  relexpfld  15005  relexpaddg  15009  shftdm  15027  rlim  15451  ramval  16973  isstruct2  17113  setsvalg  17130  setsdm  17134  prdsval  17412  homfeqbas  17656  invf  17729  dfiso2  17733  oppciso  17742  cicsym  17765  sscfn1  17778  sscfn2  17779  isssc  17781  rescval  17788  rescval2  17789  issubc  17796  issubc2  17797  cofuval  17843  resfval  17853  resfval2  17854  resf1st  17855  estrreslem2  18098  prfval  18159  lubdm  18309  glbdm  18322  joindm  18333  meetdm  18347  islat  18393  isclat  18460  oduclatb  18467  gsumvalx  18638  mndpsuppss  18727  cntzrcl  19296  f1omvdco2  19417  pmtrfrn  19427  symgsssg  19436  symgfisg  19437  symggen  19439  pmtrdifwrdellem3  19452  pmtrdifwrdel2lem1  19453  pmtrdifwrdel  19454  pmtrdifwrdel2  19455  psgnunilem1  19462  psgnunilem5  19463  psgnunilem2  19464  psgnunilem3  19465  psgneldm  19472  dmdprd  19969  dprdval  19974  dpjfval  20026  ablfaclem3  20058  cofipsgn  21586  elocv  21661  ishil  21711  dsmmval  21727  mpfrcl  22076  mamudm  22373  mavmuldm  22528  mavmul0g  22531  m1detdiag  22575  decpmatval0  22742  decpmatval  22743  pmatcollpw3lem  22761  iscnp2  23217  ptval  23548  ptcmplem2  24031  cnextfval  24040  tsmsval2  24108  ustbas2  24203  utopval  24210  tusval  24243  ucnval  24254  iscfilu  24265  psmetdmdm  24283  xmetdmdm  24313  blfvalps  24361  setsmstopn  24456  tmsval  24459  metuval  24527  tngtopn  24628  cfilfval  25244  caufval  25255  limcfval  25852  dvfval  25877  dvbsss  25882  perfdvf  25883  dvmptresicc  25896  dvn2bss  25910  dvnres  25911  dvcmul  25924  dvcmulf  25925  dvcj  25930  dvnfre  25932  dvexp  25933  dvmptres3  25936  dvmptcl  25939  dvmptadd  25940  dvmptmul  25941  dvmptres2  25942  dvmptcmul  25944  dvmptcj  25948  dvmptco  25952  rolle  25970  cmvth  25971  mvth  25972  dvlip  25973  dvlipcn  25974  dvlip2  25975  c1liplem1  25976  dveq0  25980  dv11cn  25981  dvle  25987  dvivthlem1  25988  dvivth  25990  dvne0  25991  lhop1lem  25993  lhop2  25995  lhop  25996  dvcnvrelem1  25997  dvcvx  26000  dvfsumle  26001  dvfsumge  26002  dvfsumabs  26003  dvmptrecl  26004  dvfsumlem2  26007  itgsubstlem  26028  taylfval  26338  tayl0  26341  dvtaylp  26350  dvntaylp  26351  dvntaylp0  26352  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  ulmdvlem1  26381  pserdv  26410  pige3ALT  26500  logtayl  26640  relogbf  26771  lgamgulmlem2  27010  nosupdm  27685  nosupbday  27686  nosupres  27688  nosupbnd1lem1  27689  nosupbnd1  27695  nosupbnd2  27697  noinfdm  27700  noinfbday  27701  noinfbnd1  27710  noinfbnd2  27712  perpln1  28795  isuhgr  29146  isushgr  29147  uhgreq12g  29151  isuhgrop  29156  uhgrun  29160  uhgrstrrepe  29164  isupgr  29170  upgrop  29180  isumgr  29181  upgr1e  29199  upgrun  29204  umgrun  29206  isuspgr  29238  isusgr  29239  isuspgrop  29247  isusgrop  29248  ausgrusgrb  29251  usgrstrrepe  29321  uspgr1e  29330  issubgr  29357  uhgrspansubgrlem  29376  usgrexi  29527  vtxdgfval  29554  vtxdeqd  29564  vtxdun  29568  1loopgrvd0  29591  1hevtxdg0  29592  1hevtxdg1  29593  umgr2v2e  29612  umgr2v2evd2  29614  ewlksfval  29688  wksfval  29696  wlkres  29755  wlkp1  29766  eupths  30288  eupthres  30303  trlsegvdeglem4  30311  trlsegvdeglem5  30312  grporndm  30599  hmoval  30899  gsumhashmul  33146  symgcom2  33163  symgcntz  33164  pmtrcnel2  33169  cycpmco2f1  33203  cycpmrn  33222  tocyccntz  33223  fxpval  33244  fxpgaval  33246  1arithidomlem2  33614  1arithidom  33615  minplyval  33868  smatrcl  33959  metidval  34053  pstmval  34058  prsssdm  34080  ordtrestNEW  34084  ofcfval  34261  ofcfval3  34265  brae  34404  braew  34405  faeval  34409  mbfmcst  34422  carsgval  34466  issibf  34496  sitmval  34512  0rrv  34614  dstrvprob  34635  fineqvac  35279  satfdm  35570  fmlafv  35581  fmla  35582  fmlasuc0  35585  satfdmfmla  35601  cnndvlem2  36817  bj-finsumval0  37618  cureq  37934  curf  37936  curunc  37940  sdclem2  38080  ismtyval  38138  isass  38184  isexid  38185  ismndo2  38212  exidreslem  38215  rngodm1dm2  38270  divrngcl  38295  isdrngo2  38296  cnvref4  38688  isopos  39643  isatl  39762  dibffval  41603  dibfval  41604  conrel2d  44112  iunrelexp0  44150  dmtrclfvRP  44178  rntrclfvRP  44179  neicvgbex  44560  dvsconst  44778  expgrowth  44783  fnlimfvre  46123  dvsinax  46362  dvcosax  46375  dvbdfbdioolem1  46377  itgsinexplem1  46403  itgcoscmulx  46418  dirkeritg  46551  dirkercncflem2  46553  fourierdlem60  46615  fourierdlem61  46616  fourierdlem74  46629  fourierdlem75  46630  fourierdlem80  46635  fourierdlem94  46649  fourierdlem103  46658  fourierdlem104  46659  fourierdlem113  46668  dmvon  47055  ovnovollem1  47105  smflimlem3  47222  smflimlem4  47223  smflim  47226  smflim2  47255  smfpimcc  47257  smflimmpt  47259  smfsuplem2  47261  smfsuplem3  47262  smfsup  47263  smfsupmpt  47264  smfinflem  47266  smfinf  47267  smfinfmpt  47268  smflimsuplem1  47269  smflimsuplem2  47270  smflimsuplem3  47271  smflimsuplem4  47272  smflimsuplem7  47275  smflimsup  47277  smflimsupmpt  47278  smfliminf  47280  smfliminfmpt  47281  dfateq12d  47589  isubgruhgr  48359  grimidvtxedg  48376  ushggricedg  48418  isubgrgrim  48420  stgrusgra  48450  gpgiedgdmel  48540  gpgusgra  48548  upwlksfval  48626  dmrnxp  49327  lubeldm2d  49448  glbeldm2d  49449  glbprlem  49455  isclatd  49473  isopropdlem  49530  dmdm  49543  infsubc2  49551  infsubc2d  49552  oppfvalg  49616  reldmprcof1  49871  reldmprcof2  49872  dfinito4  49991  reldmlan2  50107  reldmran2  50108  termolmd  50160