Theorem dmeqi 5846

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

Syntax hints:   = wceq 1547  dom cdm 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-dm 5628

This theorem is referenced by:  dmxpin  5873  rncoss  5919  rncoeq  5924  rnun  6096  rnin  6097  rnxp  6121  rnxpss  6123  imainrect  6132  dmpropg  6166  dmtpop  6169  rnsnopg  6172  fntpg  6545  opabiotadm  6908  dffv2  6922  fvopab4ndm  6966  fnreseql  6989  dmoprab  7459  reldmmpo  7490  mpondm0  7596  elmpocl  7597  opabn1stprc  8000  bropopvvv  8029  bropfvvvv  8031  frrlem7  8232  frrlem14  8239  tfrlem8  8313  tfr1a  8323  tfr2a  8324  tfr2b  8325  rdgseg  8351  xpassen  8999  sbthlem5  9019  hartogslem1  9447  dmttrcl  9633  r1funlim  9681  r1sucg  9684  r1limg  9686  rankf  9709  hsmexlem4  10342  axdc2lem  10361  dmaddpi  10804  dmmulpi  10805  dmaddsr  10999  dmmulsr  11000  axaddf  11059  axmulf  11060  divsfval  17502  mvdco  19411  symgsssg  19433  symgfisg  19434  pmtrdifellem2  19443  psgnunilem5  19460  ismbl  25511  volres  25513  efcvx  26432  dvrelog  26619  dvlog  26633  nosupcbv  27684  noinfcbv  27699  noetasuplem4  27718  noetainflem4  27722  dmcuts  27801  structiedg0val  29109  snstriedgval  29125  isuhgr  29147  isushgr  29148  isupgr  29171  isumgr  29182  isuspgr  29239  isusgr  29240  ushgredgedg  29316  ushgredgedgloop  29318  lfuhgr1v0e  29341  issubgr  29358  subgruhgredgd  29371  subumgredg2  29372  vtxdgfval  29554  vtxdlfgrval  29572  vtxdginducedm1lem2  29627  vtxdginducedm1fi  29631  finsumvtxdg2ssteplem4  29635  finsumvtxdg2size  29637  wlk2v2elem1  30243  dfhnorm2  31211  hlimcaui  31325  hhshsslem1  31356  dmadjss  31976  adjeu  31978  adj1o  31983  gsummpt2co  33129  cycpmrn  33224  tocyccntz  33225  extdgfialglem1  33876  prsdm  34098  mbfmcst  34443  eulerpartlemt  34555  0rrv  34635  coinflipspace  34665  bnj96  35047  bnj1398  35216  bnj1416  35221  bnj1450  35232  bnj1498  35243  bnj1501  35249  fineqvnttrclse  35305  fmla  35609  fmla0  35610  gonan0  35620  satffunlem2lem2  35634  fixun  36135  linedegen  36371  matunitlindf  37985  ssbnd  38155  ismgmOLD  38217  exidreslem  38244  n0el2  38702  dmxrn  38754  dmxrncnvepres  38799  dfsucmap2  38831  dmcoss3  38910  dmcoels  38914  dmmzp  43182  cnvrcl0  44069  dvsid  44775  dvsef  44776  modelaxreplem2  45423  dvsinax  46356  fperdvper  46362  dvcosax  46369  stoweidlem27  46470  fourierdlem57  46606  fourierdlem58  46607  fourierdlem62  46611  fourierdlem80  46629  fourierdlem94  46643  fourierdlem97  46646  fourierdlem113  46662  fouriersw  46674  fouriercn  46675  subsaliuncllem  46800  0ome  46972  hoi2toco  47050  isgrim  48373  usgrexmpl1lem  48512  usgrexmpl2lem  48517  gpgprismgr4cycllem8  48593  elbigofrcl  49041  dmtposss  49366  initocmd  50159  termolmd  50160