Theorem dmeqi 5894

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

Syntax hints:   = wceq 1570  dom cdm 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-dm 5671

This theorem is referenced by:  dmxpin  5921  rncoss  5967  rncoeq  5971  rnun  6142  rninOLD  6144  rnxp  6168  rnxpss  6170  imainrect  6179  dmpropg  6216  dmtpop  6219  rnsnopg  6222  fntpg  6596  opabiotadm  6962  dffv2  6976  fvopab4ndm  7020  fnreseql  7043  dmoprab  7513  reldmmpo  7544  mpondm0  7650  elmpocl  7651  opabn1stprc  8051  bropopvvv  8081  bropfvvvv  8083  frrlem7  8285  frrlem14  8292  tfrlem8  8367  tfr1a  8377  tfr2a  8378  tfr2b  8379  rdgseg  8405  xpassen  9055  sbthlem5  9075  hartogslem1  9500  dmttrcl  9686  r1funlim  9734  r1sucg  9737  r1limg  9739  rankf  9762  hsmexlem4  10408  axdc2lem  10427  dmaddpi  10870  dmmulpi  10871  dmaddsr  11065  dmmulsr  11066  axaddf  11125  axmulf  11126  divsfval  17596  mvdco  19510  symgsssg  19532  symgfisg  19533  pmtrdifellem2  19542  psgnunilem5  19559  ismbl  25685  volres  25687  efcvx  26612  dvrelog  26802  dvlog  26816  nosupcbv  27866  noinfcbv  27881  noetasuplem4  27900  noetainflem4  27904  dmcuts  27984  structiedg0val  29372  snstriedgval  29388  isuhgr  29410  isushgr  29411  isupgr  29434  isumgr  29445  isuspgr  29502  isusgr  29503  ushgredgedg  29579  ushgredgedgloop  29581  lfuhgr1v0e  29604  issubgr  29621  subgruhgredgd  29634  subumgredg2  29635  vtxdgfval  29817  vtxdlfgrval  29835  vtxdginducedm1lem2  29890  vtxdginducedm1fi  29894  finsumvtxdg2ssteplem4  29898  finsumvtxdg2size  29900  wlk2v2elem1  30506  dfhnorm2  31474  hlimcaui  31588  hhshsslem1  31619  dmadjss  32239  adjeu  32241  adj1o  32246  gsummpt2co  33368  cycpmrn  33463  tocyccntz  33464  extdgfialglem1  34082  prsdm  34304  mbfmcst  34649  eulerpartlemt  34761  0rrv  34841  coinflipspace  34871  bnj96  35253  bnj1398  35422  bnj1416  35427  bnj1450  35438  bnj1498  35449  bnj1501  35455  fineqvnttrclse  35537  fmla  35873  fmla0  35874  gonan0  35884  satffunlem2lem2  35898  fixun  36399  linedegen  36635  matunitlindf  38269  ssbnd  38439  ismgmOLD  38501  exidreslem  38528  n0el2  38984  dmxrn  39036  dmxrncnvepres  39081  dfsucmap2  39113  dmcoss3  39192  dmcoels  39196  dmmzp  43464  cnvrcl0  44351  dvsid  45041  dvsef  45042  modelaxreplem2  45688  dvsinax  46627  fperdvper  46633  dvcosax  46640  stoweidlem27  46741  fourierdlem57  46877  fourierdlem58  46878  fourierdlem62  46882  fourierdlem80  46900  fourierdlem94  46914  fourierdlem97  46917  fourierdlem113  46933  fouriersw  46945  fouriercn  46946  subsaliuncllem  47071  0ome  47243  hoi2toco  47321  isgrim  48647  usgrexmpl1lem  48786  usgrexmpl2lem  48791  gpgprismgr4cycllem8  48867  elbigofrcl  49330  dmtposss  49654  initocmd  50447  termolmd  50448