Theorem dmeqi 5859

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

Syntax hints:   = wceq 1542  dom cdm 5631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-dm 5641

This theorem is referenced by:  dmxpin  5886  rncoss  5932  rncoeq  5937  rnun  6109  rnin  6110  rnxp  6134  rnxpss  6136  imainrect  6145  dmpropg  6179  dmtpop  6182  rnsnopg  6185  fntpg  6558  opabiotadm  6921  dffv2  6935  fvopab4ndm  6978  fnreseql  7000  dmoprab  7470  reldmmpo  7501  mpondm0  7607  elmpocl  7608  opabn1stprc  8011  bropopvvv  8040  bropfvvvv  8042  frrlem7  8242  frrlem14  8249  tfrlem8  8323  tfr1a  8333  tfr2a  8334  tfr2b  8335  rdgseg  8361  xpassen  9009  sbthlem5  9029  hartogslem1  9457  dmttrcl  9642  r1funlim  9690  r1sucg  9693  r1limg  9695  rankf  9718  hsmexlem4  10351  axdc2lem  10370  dmaddpi  10813  dmmulpi  10814  dmaddsr  11008  dmmulsr  11009  axaddf  11068  axmulf  11069  divsfval  17511  mvdco  19420  symgsssg  19442  symgfisg  19443  pmtrdifellem2  19452  psgnunilem5  19469  ismbl  25493  volres  25495  efcvx  26414  dvrelog  26601  dvlog  26615  nosupcbv  27666  noinfcbv  27681  noetasuplem4  27700  noetainflem4  27704  dmcuts  27783  structiedg0val  29091  snstriedgval  29107  isuhgr  29129  isushgr  29130  isupgr  29153  isumgr  29164  isuspgr  29221  isusgr  29222  ushgredgedg  29298  ushgredgedgloop  29300  lfuhgr1v0e  29323  issubgr  29340  subgruhgredgd  29353  subumgredg2  29354  vtxdgfval  29536  vtxdlfgrval  29554  vtxdginducedm1lem2  29609  vtxdginducedm1fi  29613  finsumvtxdg2ssteplem4  29617  finsumvtxdg2size  29619  wlk2v2elem1  30225  dfhnorm2  31193  hlimcaui  31307  hhshsslem1  31338  dmadjss  31958  adjeu  31960  adj1o  31965  gsummpt2co  33109  cycpmrn  33204  tocyccntz  33205  extdgfialglem1  33836  prsdm  34058  mbfmcst  34403  eulerpartlemt  34515  0rrv  34595  coinflipspace  34625  bnj96  35007  bnj1398  35176  bnj1416  35181  bnj1450  35192  bnj1498  35203  bnj1501  35209  fineqvnttrclse  35268  fmla  35563  fmla0  35564  gonan0  35574  satffunlem2lem2  35588  fixun  36089  linedegen  36325  matunitlindf  37939  ssbnd  38109  ismgmOLD  38171  exidreslem  38198  n0el2  38656  dmxrn  38708  dmxrncnvepres  38753  dfsucmap2  38785  dmcoss3  38864  dmcoels  38868  dmmzp  43165  cnvrcl0  44052  dvsid  44758  dvsef  44759  modelaxreplem2  45406  dvsinax  46341  fperdvper  46347  dvcosax  46354  stoweidlem27  46455  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fourierdlem80  46614  fourierdlem94  46628  fourierdlem97  46631  fourierdlem113  46647  fouriersw  46659  fouriercn  46660  subsaliuncllem  46785  0ome  46957  hoi2toco  47035  isgrim  48358  usgrexmpl1lem  48497  usgrexmpl2lem  48502  gpgprismgr4cycllem8  48578  elbigofrcl  49026  dmtposss  49351  initocmd  50144  termolmd  50145