Theorem dmeqi 5858

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

Syntax hints:   = wceq 1540  dom cdm 5631

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-dm 5641

This theorem is referenced by:  dmxpin  5884  rncoss  5928  rncoeq  5932  rnun  6106  rnin  6107  rnxp  6131  rnxpss  6133  imainrect  6142  dmpropg  6176  dmtpop  6179  rnsnopg  6182  fntpg  6560  opabiotadm  6924  dffv2  6938  fvopab4ndm  6980  fnreseql  7002  dmoprab  7472  reldmmpo  7503  mpondm0  7609  elmpocl  7610  opabn1stprc  8016  bropopvvv  8046  bropfvvvv  8048  frrlem7  8248  frrlem14  8255  tfrlem8  8329  tfr1a  8339  tfr2a  8340  tfr2b  8341  rdgseg  8367  xpassen  9012  sbthlem5  9032  hartogslem1  9471  dmttrcl  9650  r1funlim  9695  r1sucg  9698  r1limg  9700  rankf  9723  hsmexlem4  10358  axdc2lem  10377  dmaddpi  10819  dmmulpi  10820  dmaddsr  11014  dmmulsr  11015  axaddf  11074  axmulf  11075  divsfval  17486  mvdco  19351  symgsssg  19373  symgfisg  19374  pmtrdifellem2  19383  psgnunilem5  19400  ismbl  25403  volres  25405  efcvx  26335  dvrelog  26522  dvlog  26536  nosupcbv  27590  noinfcbv  27605  noetasuplem4  27624  noetainflem4  27628  dmscut  27699  structiedg0val  28925  snstriedgval  28941  isuhgr  28963  isushgr  28964  isupgr  28987  isumgr  28998  isuspgr  29055  isusgr  29056  ushgredgedg  29132  ushgredgedgloop  29134  lfuhgr1v0e  29157  issubgr  29174  subgruhgredgd  29187  subumgredg2  29188  vtxdgfval  29371  vtxdlfgrval  29389  vtxdginducedm1lem2  29444  vtxdginducedm1fi  29448  finsumvtxdg2ssteplem4  29452  finsumvtxdg2size  29454  wlk2v2elem1  30057  dfhnorm2  31024  hlimcaui  31138  hhshsslem1  31169  dmadjss  31789  adjeu  31791  adj1o  31796  gsummpt2co  32961  cycpmrn  33073  tocyccntz  33074  prsdm  33877  mbfmcst  34223  eulerpartlemt  34335  0rrv  34415  coinflipspace  34445  bnj96  34828  bnj1398  34997  bnj1416  35002  bnj1450  35013  bnj1498  35024  bnj1501  35030  fmla  35341  fmla0  35342  gonan0  35352  satffunlem2lem2  35366  fixun  35870  linedegen  36104  matunitlindf  37585  ssbnd  37755  ismgmOLD  37817  exidreslem  37844  n0el2  38290  dmxrn  38333  dmxrncnvepres  38368  dmcoss3  38417  dmcoels  38421  dmmzp  42694  cnvrcl0  43587  dvsid  44293  dvsef  44294  modelaxreplem2  44942  dvsinax  45884  fperdvper  45890  dvcosax  45897  stoweidlem27  45998  fourierdlem57  46134  fourierdlem58  46135  fourierdlem62  46139  fourierdlem80  46157  fourierdlem94  46171  fourierdlem97  46174  fourierdlem113  46190  fouriersw  46202  fouriercn  46203  subsaliuncllem  46328  0ome  46500  hoi2toco  46578  isgrim  47855  usgrexmpl1lem  47985  usgrexmpl2lem  47990  gpgprismgr4cycllem8  48065  elbigofrcl  48512  dmtposss  48837  initocmd  49631  termolmd  49632