Theorem dmeqi 5929

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

Syntax hints:   = wceq 1537  dom cdm 5700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-dm 5710

This theorem is referenced by:  dmxpOLD  5954  dmxpin  5956  rncoss  5998  rncoeq  6002  rnun  6177  rnin  6178  rnxp  6201  rnxpss  6203  imainrect  6212  dmpropg  6246  dmtpop  6249  rnsnopg  6252  fntpg  6638  opabiotadm  7003  dffv2  7017  fvopab4ndm  7059  fnreseql  7081  dmoprab  7552  reldmmpo  7584  mpondm0  7690  elmpocl  7691  opabn1stprc  8099  bropopvvv  8131  bropfvvvv  8133  frrlem7  8333  frrlem14  8340  wfrdmssOLD  8371  wfrdmclOLD  8373  wfrlem16OLD  8380  tfrlem8  8440  tfr1a  8450  tfr2a  8451  tfr2b  8452  rdgseg  8478  xpassen  9132  sbthlem5  9153  hartogslem1  9611  dmttrcl  9790  r1funlim  9835  r1sucg  9838  r1limg  9840  rankf  9863  hsmexlem4  10498  axdc2lem  10517  dmaddpi  10959  dmmulpi  10960  dmaddsr  11154  dmmulsr  11155  axaddf  11214  axmulf  11215  divsfval  17607  mvdco  19487  symgsssg  19509  symgfisg  19510  pmtrdifellem2  19519  psgnunilem5  19536  ismbl  25580  volres  25582  efcvx  26511  dvrelog  26697  dvlog  26711  nosupcbv  27765  noinfcbv  27780  noetasuplem4  27799  noetainflem4  27803  dmscut  27874  structiedg0val  29057  snstriedgval  29073  isuhgr  29095  isushgr  29096  isupgr  29119  isumgr  29130  isuspgr  29187  isusgr  29188  ushgredgedg  29264  ushgredgedgloop  29266  lfuhgr1v0e  29289  issubgr  29306  subgruhgredgd  29319  subumgredg2  29320  vtxdgfval  29503  vtxdlfgrval  29521  vtxdginducedm1lem2  29576  vtxdginducedm1fi  29580  finsumvtxdg2ssteplem4  29584  finsumvtxdg2size  29586  wlk2v2elem1  30187  dfhnorm2  31154  hlimcaui  31268  hhshsslem1  31299  dmadjss  31919  adjeu  31921  adj1o  31926  gsummpt2co  33031  cycpmrn  33136  tocyccntz  33137  prsdm  33860  mbfmcst  34224  eulerpartlemt  34336  0rrv  34416  coinflipspace  34445  bnj96  34841  bnj1398  35010  bnj1416  35015  bnj1450  35026  bnj1498  35037  bnj1501  35043  fmla  35349  fmla0  35350  gonan0  35360  satffunlem2lem2  35374  fixun  35873  linedegen  36107  matunitlindf  37578  ssbnd  37748  ismgmOLD  37810  exidreslem  37837  n0el2  38289  dmcoss3  38409  dmcoels  38413  dmmzp  42689  cnvrcl0  43587  dvsid  44300  dvsef  44301  dvsinax  45834  fperdvper  45840  dvcosax  45847  stoweidlem27  45948  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fourierdlem80  46107  fourierdlem94  46121  fourierdlem97  46124  fourierdlem113  46140  fouriersw  46152  fouriercn  46153  subsaliuncllem  46278  0ome  46450  hoi2toco  46528  isgrim  47752  usgrexmpl1lem  47836  usgrexmpl2lem  47841  elbigofrcl  48284