Theorem dmeqi 5816

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

Syntax hints:   = wceq 1539  dom cdm 5590

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-dm 5600

This theorem is referenced by:  dmxp  5841  dmxpin  5843  rncoss  5884  rncoeq  5887  rnun  6054  rnin  6055  rnxp  6078  rnxpss  6080  imainrect  6089  dmpropg  6123  dmtpop  6126  rnsnopg  6129  fntpg  6501  opabiotadm  6859  dffv2  6872  fvopab4ndm  6913  fnreseql  6934  dmoprab  7385  reldmmpo  7417  mpondm0  7519  elmpocl  7520  opabn1stprc  7907  bropopvvv  7939  bropfvvvv  7941  frrlem7  8117  frrlem14  8124  wfrdmssOLD  8155  wfrdmclOLD  8157  wfrlem16OLD  8164  tfrlem8  8224  tfr1a  8234  tfr2a  8235  tfr2b  8236  rdgseg  8262  xpassen  8862  sbthlem5  8883  hartogslem1  9310  dmttrcl  9488  r1funlim  9533  r1sucg  9536  r1limg  9538  rankf  9561  hsmexlem4  10194  axdc2lem  10213  dmaddpi  10655  dmmulpi  10656  dmaddsr  10850  dmmulsr  10851  axaddf  10910  axmulf  10911  divsfval  17267  mvdco  19062  symgsssg  19084  symgfisg  19085  pmtrdifellem2  19094  psgnunilem5  19111  ismbl  24699  volres  24701  efcvx  25617  dvrelog  25801  dvlog  25815  structiedg0val  27401  snstriedgval  27417  isuhgr  27439  isushgr  27440  isupgr  27463  isumgr  27474  isuspgr  27531  isusgr  27532  ushgredgedg  27605  ushgredgedgloop  27607  lfuhgr1v0e  27630  issubgr  27647  subgruhgredgd  27660  subumgredg2  27661  vtxdgfval  27843  vtxdlfgrval  27861  vtxdginducedm1lem2  27916  vtxdginducedm1fi  27920  finsumvtxdg2ssteplem4  27924  finsumvtxdg2size  27926  wlk2v2elem1  28528  dfhnorm2  29493  hlimcaui  29607  hhshsslem1  29638  dmadjss  30258  adjeu  30260  adj1o  30265  gsummpt2co  31317  cycpmrn  31419  tocyccntz  31420  prsdm  31873  mbfmcst  32235  eulerpartlemt  32347  0rrv  32427  coinflipspace  32456  bnj96  32854  bnj1398  33023  bnj1416  33028  bnj1450  33039  bnj1498  33050  bnj1501  33056  fmla  33352  fmla0  33353  gonan0  33363  satffunlem2lem2  33377  nosupcbv  33914  noinfcbv  33929  noetasuplem4  33948  noetainflem4  33952  dmscut  34014  fixun  34220  linedegen  34454  matunitlindf  35784  ssbnd  35955  ismgmOLD  36017  exidreslem  36044  n0el2  36475  dmcoss3  36578  dmcoels  36582  dmmzp  40562  cnvrcl0  41240  dvsid  41956  dvsef  41957  dvsinax  43461  fperdvper  43467  dvcosax  43474  stoweidlem27  43575  fourierdlem57  43711  fourierdlem58  43712  fourierdlem62  43716  fourierdlem80  43734  fourierdlem94  43748  fourierdlem97  43751  fourierdlem113  43767  fouriersw  43779  fouriercn  43780  subsaliuncllem  43903  0ome  44074  hoi2toco  44152  elbigofrcl  45907