Theorem dmeqi 5853

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

Syntax hints:   = wceq 1541  dom cdm 5624

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-dm 5634

This theorem is referenced by:  dmxpin  5880  rncoss  5926  rncoeq  5931  rnun  6103  rnin  6104  rnxp  6128  rnxpss  6130  imainrect  6139  dmpropg  6173  dmtpop  6176  rnsnopg  6179  fntpg  6552  opabiotadm  6915  dffv2  6929  fvopab4ndm  6971  fnreseql  6993  dmoprab  7461  reldmmpo  7492  mpondm0  7598  elmpocl  7599  opabn1stprc  8002  bropopvvv  8032  bropfvvvv  8034  frrlem7  8234  frrlem14  8241  tfrlem8  8315  tfr1a  8325  tfr2a  8326  tfr2b  8327  rdgseg  8353  xpassen  8999  sbthlem5  9019  hartogslem1  9447  dmttrcl  9630  r1funlim  9678  r1sucg  9681  r1limg  9683  rankf  9706  hsmexlem4  10339  axdc2lem  10358  dmaddpi  10801  dmmulpi  10802  dmaddsr  10996  dmmulsr  10997  axaddf  11056  axmulf  11057  divsfval  17468  mvdco  19374  symgsssg  19396  symgfisg  19397  pmtrdifellem2  19406  psgnunilem5  19423  ismbl  25483  volres  25485  efcvx  26415  dvrelog  26602  dvlog  26616  nosupcbv  27670  noinfcbv  27685  noetasuplem4  27704  noetainflem4  27708  dmcuts  27787  structiedg0val  29095  snstriedgval  29111  isuhgr  29133  isushgr  29134  isupgr  29157  isumgr  29168  isuspgr  29225  isusgr  29226  ushgredgedg  29302  ushgredgedgloop  29304  lfuhgr1v0e  29327  issubgr  29344  subgruhgredgd  29357  subumgredg2  29358  vtxdgfval  29541  vtxdlfgrval  29559  vtxdginducedm1lem2  29614  vtxdginducedm1fi  29618  finsumvtxdg2ssteplem4  29622  finsumvtxdg2size  29624  wlk2v2elem1  30230  dfhnorm2  31197  hlimcaui  31311  hhshsslem1  31342  dmadjss  31962  adjeu  31964  adj1o  31969  gsummpt2co  33131  cycpmrn  33225  tocyccntz  33226  extdgfialglem1  33849  prsdm  34071  mbfmcst  34416  eulerpartlemt  34528  0rrv  34608  coinflipspace  34638  bnj96  35021  bnj1398  35190  bnj1416  35195  bnj1450  35206  bnj1498  35217  bnj1501  35223  fineqvnttrclse  35280  fmla  35575  fmla0  35576  gonan0  35586  satffunlem2lem2  35600  fixun  36101  linedegen  36337  matunitlindf  37819  ssbnd  37989  ismgmOLD  38051  exidreslem  38078  n0el2  38528  dmxrn  38572  dmxrncnvepres  38617  dfsucmap2  38638  dmcoss3  38716  dmcoels  38720  dmmzp  42975  cnvrcl0  43866  dvsid  44572  dvsef  44573  modelaxreplem2  45220  dvsinax  46157  fperdvper  46163  dvcosax  46170  stoweidlem27  46271  fourierdlem57  46407  fourierdlem58  46408  fourierdlem62  46412  fourierdlem80  46430  fourierdlem94  46444  fourierdlem97  46447  fourierdlem113  46463  fouriersw  46475  fouriercn  46476  subsaliuncllem  46601  0ome  46773  hoi2toco  46851  isgrim  48128  usgrexmpl1lem  48267  usgrexmpl2lem  48272  gpgprismgr4cycllem8  48348  elbigofrcl  48796  dmtposss  49121  initocmd  49914  termolmd  49915