Theorem dmeqi 5802

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

Syntax hints:   = wceq 1539  dom cdm 5580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-dm 5590

This theorem is referenced by:  dmxp  5827  dmxpin  5829  rncoss  5870  rncoeq  5873  rnun  6038  rnin  6039  rnxp  6062  rnxpss  6064  imainrect  6073  dmpropg  6107  dmtpop  6110  rnsnopg  6113  fntpg  6478  opabiotadm  6832  dffv2  6845  fvopab4ndm  6886  fnreseql  6907  dmoprab  7354  reldmmpo  7386  mpondm0  7488  elmpocl  7489  opabn1stprc  7871  bropopvvv  7901  bropfvvvv  7903  frrlem7  8079  frrlem14  8086  wfrdmssOLD  8117  wfrdmclOLD  8119  wfrlem16OLD  8126  tfrlem8  8186  tfr1a  8196  tfr2a  8197  tfr2b  8198  rdgseg  8224  xpassen  8806  sbthlem5  8827  hartogslem1  9231  r1funlim  9455  r1sucg  9458  r1limg  9460  rankf  9483  hsmexlem4  10116  axdc2lem  10135  dmaddpi  10577  dmmulpi  10578  dmaddsr  10772  dmmulsr  10773  axaddf  10832  axmulf  10833  divsfval  17175  mvdco  18968  symgsssg  18990  symgfisg  18991  pmtrdifellem2  19000  psgnunilem5  19017  ismbl  24595  volres  24597  efcvx  25513  dvrelog  25697  dvlog  25711  structiedg0val  27295  snstriedgval  27311  isuhgr  27333  isushgr  27334  isupgr  27357  isumgr  27368  isuspgr  27425  isusgr  27426  ushgredgedg  27499  ushgredgedgloop  27501  lfuhgr1v0e  27524  issubgr  27541  subgruhgredgd  27554  subumgredg2  27555  vtxdgfval  27737  vtxdlfgrval  27755  vtxdginducedm1lem2  27810  vtxdginducedm1fi  27814  finsumvtxdg2ssteplem4  27818  finsumvtxdg2size  27820  wlk2v2elem1  28420  dfhnorm2  29385  hlimcaui  29499  hhshsslem1  29530  dmadjss  30150  adjeu  30152  adj1o  30157  gsummpt2co  31210  cycpmrn  31312  tocyccntz  31313  prsdm  31766  mbfmcst  32126  eulerpartlemt  32238  0rrv  32318  coinflipspace  32347  bnj96  32745  bnj1398  32914  bnj1416  32919  bnj1450  32930  bnj1498  32941  bnj1501  32947  fmla  33243  fmla0  33244  gonan0  33254  satffunlem2lem2  33268  dmttrcl  33707  nosupcbv  33832  noinfcbv  33847  noetasuplem4  33866  noetainflem4  33870  dmscut  33932  fixun  34138  linedegen  34372  matunitlindf  35702  ssbnd  35873  ismgmOLD  35935  exidreslem  35962  n0el2  36395  dmcoss3  36498  dmcoels  36502  dmmzp  40471  cnvrcl0  41122  dvsid  41838  dvsef  41839  dvsinax  43344  fperdvper  43350  dvcosax  43357  stoweidlem27  43458  fourierdlem57  43594  fourierdlem58  43595  fourierdlem62  43599  fourierdlem80  43617  fourierdlem94  43631  fourierdlem97  43634  fourierdlem113  43650  fouriersw  43662  fouriercn  43663  subsaliuncllem  43786  0ome  43957  hoi2toco  44035  elbigofrcl  45784