Theorem dmeqi 5876

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

Syntax hints:   = wceq 1559  dom cdm 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-dm 5653

This theorem is referenced by:  dmxpin  5903  rncoss  5949  rncoeq  5954  rnun  6125  rninOLD  6127  rnxp  6151  rnxpss  6153  imainrect  6162  dmpropg  6197  dmtpop  6200  rnsnopg  6203  fntpg  6576  opabiotadm  6943  dffv2  6957  fvopab4ndm  7001  fnreseql  7024  dmoprab  7494  reldmmpo  7525  mpondm0  7631  elmpocl  7632  opabn1stprc  8034  bropopvvv  8063  bropfvvvv  8065  frrlem7  8267  frrlem14  8274  tfrlem8  8349  tfr1a  8359  tfr2a  8360  tfr2b  8361  rdgseg  8387  xpassen  9037  sbthlem5  9057  hartogslem1  9484  dmttrcl  9670  r1funlim  9718  r1sucg  9721  r1limg  9723  rankf  9746  hsmexlem4  10380  axdc2lem  10399  dmaddpi  10842  dmmulpi  10843  dmaddsr  11037  dmmulsr  11038  axaddf  11097  axmulf  11098  divsfval  17568  mvdco  19476  symgsssg  19498  symgfisg  19499  pmtrdifellem2  19508  psgnunilem5  19525  ismbl  25576  volres  25578  efcvx  26500  dvrelog  26690  dvlog  26704  nosupcbv  27754  noinfcbv  27769  noetasuplem4  27788  noetainflem4  27792  dmcuts  27872  structiedg0val  29180  snstriedgval  29196  isuhgr  29218  isushgr  29219  isupgr  29242  isumgr  29253  isuspgr  29310  isusgr  29311  ushgredgedg  29387  ushgredgedgloop  29389  lfuhgr1v0e  29412  issubgr  29429  subgruhgredgd  29442  subumgredg2  29443  vtxdgfval  29625  vtxdlfgrval  29643  vtxdginducedm1lem2  29698  vtxdginducedm1fi  29702  finsumvtxdg2ssteplem4  29706  finsumvtxdg2size  29708  wlk2v2elem1  30314  dfhnorm2  31282  hlimcaui  31396  hhshsslem1  31427  dmadjss  32047  adjeu  32049  adj1o  32054  gsummpt2co  33189  cycpmrn  33284  tocyccntz  33285  extdgfialglem1  33950  prsdm  34172  mbfmcst  34517  eulerpartlemt  34629  0rrv  34709  coinflipspace  34739  bnj96  35121  bnj1398  35290  bnj1416  35295  bnj1450  35306  bnj1498  35317  bnj1501  35323  fineqvnttrclse  35381  fmla  35692  fmla0  35693  gonan0  35703  satffunlem2lem2  35717  fixun  36218  linedegen  36454  matunitlindf  38078  ssbnd  38248  ismgmOLD  38310  exidreslem  38337  n0el2  38795  dmxrn  38847  dmxrncnvepres  38892  dfsucmap2  38924  dmcoss3  39003  dmcoels  39007  dmmzp  43275  cnvrcl0  44162  dvsid  44868  dvsef  44869  modelaxreplem2  45516  dvsinax  46448  fperdvper  46454  dvcosax  46461  stoweidlem27  46562  fourierdlem57  46698  fourierdlem58  46699  fourierdlem62  46703  fourierdlem80  46721  fourierdlem94  46735  fourierdlem97  46738  fourierdlem113  46754  fouriersw  46766  fouriercn  46767  subsaliuncllem  46892  0ome  47064  hoi2toco  47142  isgrim  48465  usgrexmpl1lem  48604  usgrexmpl2lem  48609  gpgprismgr4cycllem8  48685  elbigofrcl  49133  dmtposss  49458  initocmd  50251  termolmd  50252