Theorem dmeqi 5903

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 5902	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐴 = dom 𝐵

Syntax hints:   = wceq 1542  dom cdm 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-dm 5686

This theorem is referenced by:  dmxp  5927  dmxpin  5929  rncoss  5970  rncoeq  5973  rnun  6143  rnin  6144  rnxp  6167  rnxpss  6169  imainrect  6178  dmpropg  6212  dmtpop  6215  rnsnopg  6218  fntpg  6606  opabiotadm  6971  dffv2  6984  fvopab4ndm  7025  fnreseql  7047  dmoprab  7507  reldmmpo  7540  mpondm0  7644  elmpocl  7645  opabn1stprc  8041  bropopvvv  8073  bropfvvvv  8075  frrlem7  8274  frrlem14  8281  wfrdmssOLD  8312  wfrdmclOLD  8314  wfrlem16OLD  8321  tfrlem8  8381  tfr1a  8391  tfr2a  8392  tfr2b  8393  rdgseg  8419  xpassen  9063  sbthlem5  9084  hartogslem1  9534  dmttrcl  9713  r1funlim  9758  r1sucg  9761  r1limg  9763  rankf  9786  hsmexlem4  10421  axdc2lem  10440  dmaddpi  10882  dmmulpi  10883  dmaddsr  11077  dmmulsr  11078  axaddf  11137  axmulf  11138  divsfval  17490  mvdco  19308  symgsssg  19330  symgfisg  19331  pmtrdifellem2  19340  psgnunilem5  19357  ismbl  25035  volres  25037  efcvx  25953  dvrelog  26137  dvlog  26151  nosupcbv  27195  noinfcbv  27210  noetasuplem4  27229  noetainflem4  27233  dmscut  27302  structiedg0val  28272  snstriedgval  28288  isuhgr  28310  isushgr  28311  isupgr  28334  isumgr  28345  isuspgr  28402  isusgr  28403  ushgredgedg  28476  ushgredgedgloop  28478  lfuhgr1v0e  28501  issubgr  28518  subgruhgredgd  28531  subumgredg2  28532  vtxdgfval  28714  vtxdlfgrval  28732  vtxdginducedm1lem2  28787  vtxdginducedm1fi  28791  finsumvtxdg2ssteplem4  28795  finsumvtxdg2size  28797  wlk2v2elem1  29398  dfhnorm2  30363  hlimcaui  30477  hhshsslem1  30508  dmadjss  31128  adjeu  31130  adj1o  31135  gsummpt2co  32188  cycpmrn  32290  tocyccntz  32291  prsdm  32883  mbfmcst  33247  eulerpartlemt  33359  0rrv  33439  coinflipspace  33468  bnj96  33865  bnj1398  34034  bnj1416  34039  bnj1450  34050  bnj1498  34061  bnj1501  34067  fmla  34361  fmla0  34362  gonan0  34372  satffunlem2lem2  34386  fixun  34870  linedegen  35104  matunitlindf  36475  ssbnd  36645  ismgmOLD  36707  exidreslem  36734  n0el2  37191  dmcoss3  37312  dmcoels  37316  dmmzp  41457  cnvrcl0  42362  dvsid  43076  dvsef  43077  dvsinax  44616  fperdvper  44622  dvcosax  44629  stoweidlem27  44730  fourierdlem57  44866  fourierdlem58  44867  fourierdlem62  44871  fourierdlem80  44889  fourierdlem94  44903  fourierdlem97  44906  fourierdlem113  44922  fouriersw  44934  fouriercn  44935  subsaliuncllem  45060  0ome  45232  hoi2toco  45310  elbigofrcl  47190