Theorem dmeqi 5905

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

Syntax hints:   = wceq 1542  dom cdm 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-dm 5687

This theorem is referenced by:  dmxp  5929  dmxpin  5931  rncoss  5972  rncoeq  5975  rnun  6146  rnin  6147  rnxp  6170  rnxpss  6172  imainrect  6181  dmpropg  6215  dmtpop  6218  rnsnopg  6221  fntpg  6609  opabiotadm  6974  dffv2  6987  fvopab4ndm  7028  fnreseql  7050  dmoprab  7510  reldmmpo  7543  mpondm0  7647  elmpocl  7648  opabn1stprc  8044  bropopvvv  8076  bropfvvvv  8078  frrlem7  8277  frrlem14  8284  wfrdmssOLD  8315  wfrdmclOLD  8317  wfrlem16OLD  8324  tfrlem8  8384  tfr1a  8394  tfr2a  8395  tfr2b  8396  rdgseg  8422  xpassen  9066  sbthlem5  9087  hartogslem1  9537  dmttrcl  9716  r1funlim  9761  r1sucg  9764  r1limg  9766  rankf  9789  hsmexlem4  10424  axdc2lem  10443  dmaddpi  10885  dmmulpi  10886  dmaddsr  11080  dmmulsr  11081  axaddf  11140  axmulf  11141  divsfval  17493  mvdco  19313  symgsssg  19335  symgfisg  19336  pmtrdifellem2  19345  psgnunilem5  19362  ismbl  25043  volres  25045  efcvx  25961  dvrelog  26145  dvlog  26159  nosupcbv  27205  noinfcbv  27220  noetasuplem4  27239  noetainflem4  27243  dmscut  27312  structiedg0val  28282  snstriedgval  28298  isuhgr  28320  isushgr  28321  isupgr  28344  isumgr  28355  isuspgr  28412  isusgr  28413  ushgredgedg  28486  ushgredgedgloop  28488  lfuhgr1v0e  28511  issubgr  28528  subgruhgredgd  28541  subumgredg2  28542  vtxdgfval  28724  vtxdlfgrval  28742  vtxdginducedm1lem2  28797  vtxdginducedm1fi  28801  finsumvtxdg2ssteplem4  28805  finsumvtxdg2size  28807  wlk2v2elem1  29408  dfhnorm2  30375  hlimcaui  30489  hhshsslem1  30520  dmadjss  31140  adjeu  31142  adj1o  31147  gsummpt2co  32200  cycpmrn  32302  tocyccntz  32303  prsdm  32894  mbfmcst  33258  eulerpartlemt  33370  0rrv  33450  coinflipspace  33479  bnj96  33876  bnj1398  34045  bnj1416  34050  bnj1450  34061  bnj1498  34072  bnj1501  34078  fmla  34372  fmla0  34373  gonan0  34383  satffunlem2lem2  34397  fixun  34881  linedegen  35115  matunitlindf  36486  ssbnd  36656  ismgmOLD  36718  exidreslem  36745  n0el2  37202  dmcoss3  37323  dmcoels  37327  dmmzp  41471  cnvrcl0  42376  dvsid  43090  dvsef  43091  dvsinax  44629  fperdvper  44635  dvcosax  44642  stoweidlem27  44743  fourierdlem57  44879  fourierdlem58  44880  fourierdlem62  44884  fourierdlem80  44902  fourierdlem94  44916  fourierdlem97  44919  fourierdlem113  44935  fouriersw  44947  fouriercn  44948  subsaliuncllem  45073  0ome  45245  hoi2toco  45323  elbigofrcl  47236