Theorem dmeqi 5917

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

Syntax hints:   = wceq 1536  dom cdm 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-dm 5698

This theorem is referenced by:  dmxpOLD  5942  dmxpin  5944  rncoss  5988  rncoeq  5992  rnun  6167  rnin  6168  rnxp  6191  rnxpss  6193  imainrect  6202  dmpropg  6236  dmtpop  6239  rnsnopg  6242  fntpg  6627  opabiotadm  6989  dffv2  7003  fvopab4ndm  7045  fnreseql  7067  dmoprab  7534  reldmmpo  7566  mpondm0  7672  elmpocl  7673  opabn1stprc  8081  bropopvvv  8113  bropfvvvv  8115  frrlem7  8315  frrlem14  8322  wfrdmssOLD  8353  wfrdmclOLD  8355  wfrlem16OLD  8362  tfrlem8  8422  tfr1a  8432  tfr2a  8433  tfr2b  8434  rdgseg  8460  xpassen  9104  sbthlem5  9125  hartogslem1  9579  dmttrcl  9758  r1funlim  9803  r1sucg  9806  r1limg  9808  rankf  9831  hsmexlem4  10466  axdc2lem  10485  dmaddpi  10927  dmmulpi  10928  dmaddsr  11122  dmmulsr  11123  axaddf  11182  axmulf  11183  divsfval  17593  mvdco  19477  symgsssg  19499  symgfisg  19500  pmtrdifellem2  19509  psgnunilem5  19526  ismbl  25574  volres  25576  efcvx  26507  dvrelog  26693  dvlog  26707  nosupcbv  27761  noinfcbv  27776  noetasuplem4  27795  noetainflem4  27799  dmscut  27870  structiedg0val  29053  snstriedgval  29069  isuhgr  29091  isushgr  29092  isupgr  29115  isumgr  29126  isuspgr  29183  isusgr  29184  ushgredgedg  29260  ushgredgedgloop  29262  lfuhgr1v0e  29285  issubgr  29302  subgruhgredgd  29315  subumgredg2  29316  vtxdgfval  29499  vtxdlfgrval  29517  vtxdginducedm1lem2  29572  vtxdginducedm1fi  29576  finsumvtxdg2ssteplem4  29580  finsumvtxdg2size  29582  wlk2v2elem1  30183  dfhnorm2  31150  hlimcaui  31264  hhshsslem1  31295  dmadjss  31915  adjeu  31917  adj1o  31922  gsummpt2co  33033  cycpmrn  33145  tocyccntz  33146  prsdm  33874  mbfmcst  34240  eulerpartlemt  34352  0rrv  34432  coinflipspace  34461  bnj96  34857  bnj1398  35026  bnj1416  35031  bnj1450  35042  bnj1498  35053  bnj1501  35059  fmla  35365  fmla0  35366  gonan0  35376  satffunlem2lem2  35390  fixun  35890  linedegen  36124  matunitlindf  37604  ssbnd  37774  ismgmOLD  37836  exidreslem  37863  n0el2  38314  dmcoss3  38434  dmcoels  38438  dmmzp  42720  cnvrcl0  43614  dvsid  44326  dvsef  44327  modelaxreplem2  44943  dvsinax  45868  fperdvper  45874  dvcosax  45881  stoweidlem27  45982  fourierdlem57  46118  fourierdlem58  46119  fourierdlem62  46123  fourierdlem80  46141  fourierdlem94  46155  fourierdlem97  46158  fourierdlem113  46174  fouriersw  46186  fouriercn  46187  subsaliuncllem  46312  0ome  46484  hoi2toco  46562  isgrim  47805  usgrexmpl1lem  47915  usgrexmpl2lem  47920  elbigofrcl  48399