Theorem dmeqi 5839

Description: Equality inference for domain. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
dmeqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
dmeqi	⊢ dom 𝐴 = dom 𝐵

Proof of Theorem dmeqi

Step	Hyp	Ref	Expression
1		dmeqi.1	. 2 ⊢ 𝐴 = 𝐵
2		dmeq 5838	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐴 = dom 𝐵

Syntax hints:   = wceq 1541  dom cdm 5611

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 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-dm 5621

This theorem is referenced by:  dmxpin  5866  rncoss  5911  rncoeq  5916  rnun  6087  rnin  6088  rnxp  6112  rnxpss  6114  imainrect  6123  dmpropg  6157  dmtpop  6160  rnsnopg  6163  fntpg  6536  opabiotadm  6898  dffv2  6912  fvopab4ndm  6954  fnreseql  6976  dmoprab  7444  reldmmpo  7475  mpondm0  7581  elmpocl  7582  opabn1stprc  7985  bropopvvv  8015  bropfvvvv  8017  frrlem7  8217  frrlem14  8224  tfrlem8  8298  tfr1a  8308  tfr2a  8309  tfr2b  8310  rdgseg  8336  xpassen  8979  sbthlem5  8999  hartogslem1  9423  dmttrcl  9606  r1funlim  9654  r1sucg  9657  r1limg  9659  rankf  9682  hsmexlem4  10315  axdc2lem  10334  dmaddpi  10776  dmmulpi  10777  dmaddsr  10971  dmmulsr  10972  axaddf  11031  axmulf  11032  divsfval  17446  mvdco  19352  symgsssg  19374  symgfisg  19375  pmtrdifellem2  19384  psgnunilem5  19401  ismbl  25449  volres  25451  efcvx  26381  dvrelog  26568  dvlog  26582  nosupcbv  27636  noinfcbv  27651  noetasuplem4  27670  noetainflem4  27674  dmscut  27747  structiedg0val  28995  snstriedgval  29011  isuhgr  29033  isushgr  29034  isupgr  29057  isumgr  29068  isuspgr  29125  isusgr  29126  ushgredgedg  29202  ushgredgedgloop  29204  lfuhgr1v0e  29227  issubgr  29244  subgruhgredgd  29257  subumgredg2  29258  vtxdgfval  29441  vtxdlfgrval  29459  vtxdginducedm1lem2  29514  vtxdginducedm1fi  29518  finsumvtxdg2ssteplem4  29522  finsumvtxdg2size  29524  wlk2v2elem1  30127  dfhnorm2  31094  hlimcaui  31208  hhshsslem1  31239  dmadjss  31859  adjeu  31861  adj1o  31866  gsummpt2co  33020  cycpmrn  33104  tocyccntz  33105  extdgfialglem1  33697  prsdm  33919  mbfmcst  34264  eulerpartlemt  34376  0rrv  34456  coinflipspace  34486  bnj96  34869  bnj1398  35038  bnj1416  35043  bnj1450  35054  bnj1498  35065  bnj1501  35071  fineqvnttrclse  35136  fmla  35417  fmla0  35418  gonan0  35428  satffunlem2lem2  35442  fixun  35943  linedegen  36177  matunitlindf  37658  ssbnd  37828  ismgmOLD  37890  exidreslem  37917  n0el2  38363  dmxrn  38406  dmxrncnvepres  38441  dmcoss3  38490  dmcoels  38494  dmmzp  42766  cnvrcl0  43658  dvsid  44364  dvsef  44365  modelaxreplem2  45012  dvsinax  45951  fperdvper  45957  dvcosax  45964  stoweidlem27  46065  fourierdlem57  46201  fourierdlem58  46202  fourierdlem62  46206  fourierdlem80  46224  fourierdlem94  46238  fourierdlem97  46241  fourierdlem113  46257  fouriersw  46269  fouriercn  46270  subsaliuncllem  46395  0ome  46567  hoi2toco  46645  isgrim  47913  usgrexmpl1lem  48052  usgrexmpl2lem  48057  gpgprismgr4cycllem8  48133  elbigofrcl  48582  dmtposss  48907  initocmd  49701  termolmd  49702