Theorem dmeqi 5847

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

Syntax hints:   = wceq 1540  dom cdm 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-dm 5629

This theorem is referenced by:  dmxpin  5873  rncoss  5918  rncoeq  5923  rnun  6094  rnin  6095  rnxp  6119  rnxpss  6121  imainrect  6130  dmpropg  6164  dmtpop  6167  rnsnopg  6170  fntpg  6542  opabiotadm  6904  dffv2  6918  fvopab4ndm  6960  fnreseql  6982  dmoprab  7452  reldmmpo  7483  mpondm0  7589  elmpocl  7590  opabn1stprc  7993  bropopvvv  8023  bropfvvvv  8025  frrlem7  8225  frrlem14  8232  tfrlem8  8306  tfr1a  8316  tfr2a  8317  tfr2b  8318  rdgseg  8344  xpassen  8988  sbthlem5  9008  hartogslem1  9434  dmttrcl  9617  r1funlim  9662  r1sucg  9665  r1limg  9667  rankf  9690  hsmexlem4  10323  axdc2lem  10342  dmaddpi  10784  dmmulpi  10785  dmaddsr  10979  dmmulsr  10980  axaddf  11039  axmulf  11040  divsfval  17451  mvdco  19324  symgsssg  19346  symgfisg  19347  pmtrdifellem2  19356  psgnunilem5  19373  ismbl  25425  volres  25427  efcvx  26357  dvrelog  26544  dvlog  26558  nosupcbv  27612  noinfcbv  27627  noetasuplem4  27646  noetainflem4  27650  dmscut  27722  structiedg0val  28967  snstriedgval  28983  isuhgr  29005  isushgr  29006  isupgr  29029  isumgr  29040  isuspgr  29097  isusgr  29098  ushgredgedg  29174  ushgredgedgloop  29176  lfuhgr1v0e  29199  issubgr  29216  subgruhgredgd  29229  subumgredg2  29230  vtxdgfval  29413  vtxdlfgrval  29431  vtxdginducedm1lem2  29486  vtxdginducedm1fi  29490  finsumvtxdg2ssteplem4  29494  finsumvtxdg2size  29496  wlk2v2elem1  30099  dfhnorm2  31066  hlimcaui  31180  hhshsslem1  31211  dmadjss  31831  adjeu  31833  adj1o  31838  gsummpt2co  33001  cycpmrn  33085  tocyccntz  33086  extdgfialglem1  33659  prsdm  33881  mbfmcst  34227  eulerpartlemt  34339  0rrv  34419  coinflipspace  34449  bnj96  34832  bnj1398  35001  bnj1416  35006  bnj1450  35017  bnj1498  35028  bnj1501  35034  fmla  35354  fmla0  35355  gonan0  35365  satffunlem2lem2  35379  fixun  35883  linedegen  36117  matunitlindf  37598  ssbnd  37768  ismgmOLD  37830  exidreslem  37857  n0el2  38303  dmxrn  38346  dmxrncnvepres  38381  dmcoss3  38430  dmcoels  38434  dmmzp  42706  cnvrcl0  43598  dvsid  44304  dvsef  44305  modelaxreplem2  44953  dvsinax  45894  fperdvper  45900  dvcosax  45907  stoweidlem27  46008  fourierdlem57  46144  fourierdlem58  46145  fourierdlem62  46149  fourierdlem80  46167  fourierdlem94  46181  fourierdlem97  46184  fourierdlem113  46200  fouriersw  46212  fouriercn  46213  subsaliuncllem  46338  0ome  46510  hoi2toco  46588  isgrim  47866  usgrexmpl1lem  48005  usgrexmpl2lem  48010  gpgprismgr4cycllem8  48086  elbigofrcl  48535  dmtposss  48860  initocmd  49654  termolmd  49655