Theorem dmeqi 5868

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

Syntax hints:   = wceq 1540  dom cdm 5638

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-dm 5648

This theorem is referenced by:  dmxpOLD  5893  dmxpin  5895  rncoss  5939  rncoeq  5943  rnun  6118  rnin  6119  rnxp  6143  rnxpss  6145  imainrect  6154  dmpropg  6188  dmtpop  6191  rnsnopg  6194  fntpg  6576  opabiotadm  6942  dffv2  6956  fvopab4ndm  6998  fnreseql  7020  dmoprab  7492  reldmmpo  7523  mpondm0  7629  elmpocl  7630  opabn1stprc  8037  bropopvvv  8069  bropfvvvv  8071  frrlem7  8271  frrlem14  8278  tfrlem8  8352  tfr1a  8362  tfr2a  8363  tfr2b  8364  rdgseg  8390  xpassen  9035  sbthlem5  9055  hartogslem1  9495  dmttrcl  9674  r1funlim  9719  r1sucg  9722  r1limg  9724  rankf  9747  hsmexlem4  10382  axdc2lem  10401  dmaddpi  10843  dmmulpi  10844  dmaddsr  11038  dmmulsr  11039  axaddf  11098  axmulf  11099  divsfval  17510  mvdco  19375  symgsssg  19397  symgfisg  19398  pmtrdifellem2  19407  psgnunilem5  19424  ismbl  25427  volres  25429  efcvx  26359  dvrelog  26546  dvlog  26560  nosupcbv  27614  noinfcbv  27629  noetasuplem4  27648  noetainflem4  27652  dmscut  27723  structiedg0val  28949  snstriedgval  28965  isuhgr  28987  isushgr  28988  isupgr  29011  isumgr  29022  isuspgr  29079  isusgr  29080  ushgredgedg  29156  ushgredgedgloop  29158  lfuhgr1v0e  29181  issubgr  29198  subgruhgredgd  29211  subumgredg2  29212  vtxdgfval  29395  vtxdlfgrval  29413  vtxdginducedm1lem2  29468  vtxdginducedm1fi  29472  finsumvtxdg2ssteplem4  29476  finsumvtxdg2size  29478  wlk2v2elem1  30084  dfhnorm2  31051  hlimcaui  31165  hhshsslem1  31196  dmadjss  31816  adjeu  31818  adj1o  31823  gsummpt2co  32988  cycpmrn  33100  tocyccntz  33101  prsdm  33904  mbfmcst  34250  eulerpartlemt  34362  0rrv  34442  coinflipspace  34472  bnj96  34855  bnj1398  35024  bnj1416  35029  bnj1450  35040  bnj1498  35051  bnj1501  35057  fmla  35368  fmla0  35369  gonan0  35379  satffunlem2lem2  35393  fixun  35897  linedegen  36131  matunitlindf  37612  ssbnd  37782  ismgmOLD  37844  exidreslem  37871  n0el2  38317  dmxrn  38360  dmxrncnvepres  38395  dmcoss3  38444  dmcoels  38448  dmmzp  42721  cnvrcl0  43614  dvsid  44320  dvsef  44321  modelaxreplem2  44969  dvsinax  45911  fperdvper  45917  dvcosax  45924  stoweidlem27  46025  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  fourierdlem80  46184  fourierdlem94  46198  fourierdlem97  46201  fourierdlem113  46217  fouriersw  46229  fouriercn  46230  subsaliuncllem  46355  0ome  46527  hoi2toco  46605  isgrim  47882  usgrexmpl1lem  48012  usgrexmpl2lem  48017  gpgprismgr4cycllem8  48092  elbigofrcl  48539  dmtposss  48864  initocmd  49658  termolmd  49659