Theorem dmeqi 5915

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

Syntax hints:   = wceq 1540  dom cdm 5685

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-dm 5695

This theorem is referenced by:  dmxpOLD  5940  dmxpin  5942  rncoss  5986  rncoeq  5990  rnun  6165  rnin  6166  rnxp  6190  rnxpss  6192  imainrect  6201  dmpropg  6235  dmtpop  6238  rnsnopg  6241  fntpg  6626  opabiotadm  6990  dffv2  7004  fvopab4ndm  7046  fnreseql  7068  dmoprab  7536  reldmmpo  7567  mpondm0  7673  elmpocl  7674  opabn1stprc  8083  bropopvvv  8115  bropfvvvv  8117  frrlem7  8317  frrlem14  8324  wfrdmssOLD  8355  wfrdmclOLD  8357  wfrlem16OLD  8364  tfrlem8  8424  tfr1a  8434  tfr2a  8435  tfr2b  8436  rdgseg  8462  xpassen  9106  sbthlem5  9127  hartogslem1  9582  dmttrcl  9761  r1funlim  9806  r1sucg  9809  r1limg  9811  rankf  9834  hsmexlem4  10469  axdc2lem  10488  dmaddpi  10930  dmmulpi  10931  dmaddsr  11125  dmmulsr  11126  axaddf  11185  axmulf  11186  divsfval  17592  mvdco  19463  symgsssg  19485  symgfisg  19486  pmtrdifellem2  19495  psgnunilem5  19512  ismbl  25561  volres  25563  efcvx  26493  dvrelog  26679  dvlog  26693  nosupcbv  27747  noinfcbv  27762  noetasuplem4  27781  noetainflem4  27785  dmscut  27856  structiedg0val  29039  snstriedgval  29055  isuhgr  29077  isushgr  29078  isupgr  29101  isumgr  29112  isuspgr  29169  isusgr  29170  ushgredgedg  29246  ushgredgedgloop  29248  lfuhgr1v0e  29271  issubgr  29288  subgruhgredgd  29301  subumgredg2  29302  vtxdgfval  29485  vtxdlfgrval  29503  vtxdginducedm1lem2  29558  vtxdginducedm1fi  29562  finsumvtxdg2ssteplem4  29566  finsumvtxdg2size  29568  wlk2v2elem1  30174  dfhnorm2  31141  hlimcaui  31255  hhshsslem1  31286  dmadjss  31906  adjeu  31908  adj1o  31913  gsummpt2co  33051  cycpmrn  33163  tocyccntz  33164  prsdm  33913  mbfmcst  34261  eulerpartlemt  34373  0rrv  34453  coinflipspace  34483  bnj96  34879  bnj1398  35048  bnj1416  35053  bnj1450  35064  bnj1498  35075  bnj1501  35081  fmla  35386  fmla0  35387  gonan0  35397  satffunlem2lem2  35411  fixun  35910  linedegen  36144  matunitlindf  37625  ssbnd  37795  ismgmOLD  37857  exidreslem  37884  n0el2  38334  dmcoss3  38454  dmcoels  38458  dmmzp  42744  cnvrcl0  43638  dvsid  44350  dvsef  44351  modelaxreplem2  44996  dvsinax  45928  fperdvper  45934  dvcosax  45941  stoweidlem27  46042  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  fourierdlem80  46201  fourierdlem94  46215  fourierdlem97  46218  fourierdlem113  46234  fouriersw  46246  fouriercn  46247  subsaliuncllem  46372  0ome  46544  hoi2toco  46622  isgrim  47868  usgrexmpl1lem  47980  usgrexmpl2lem  47985  elbigofrcl  48471  dmtposss  48776