Theorem dmeqi 5888

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

This proof depends on syntax axioms:   = wceq 1570  dom cdm 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-dm 5665

This theorem is used by:  dmxpin  5915  rncoss  5961  rncoeq  5965  rnun  6136  rninOLD  6138  rnxp  6163  rnxpss  6165  imainrect  6174  dmpropg  6211  dmtpop  6214  rnsnopg  6217  fntpg  6593  opabiotadm  6959  dffv2  6973  fvopab4ndm  7017  fnreseql  7040  dmoprab  7516  reldmmpo  7547  mpondm0  7654  elmpocl  7655  opabn1stprc  8055  bropopvvv  8087  bropfvvvv  8089  frrlem7  8291  frrlem14  8298  tfrlem8  8373  tfr1a  8383  tfr2a  8384  tfr2b  8385  rdgseg  8411  xpassen  9069  sbthlem5  9089  hartogslem1  9514  dmttrcl  9700  r1funlim  9748  r1sucg  9751  r1limg  9753  rankf  9776  hsmexlem4  10431  axdc2lem  10450  dmaddpi  10899  dmmulpi  10900  dmaddsr  11094  dmmulsr  11095  axaddf  11154  axmulf  11155  divsfval  17633  mgmn0plusgf  18741  degenmgmopdm  19047  degenmgm2opdm  19051  mvdco  19572  symgsssg  19594  symgfisg  19595  pmtrdifellem2  19604  psgnunilem5  19621  matunitlindf  22903  ismbl  25754  volres  25756  efcvx  26685  dvrelog  26874  dvlog  26888  nosupcbv  27938  noinfcbv  27953  noetasuplem4  27972  noetainflem4  27976  dmcuts  28056  structiedg0val  29479  snstriedgval  29495  isuhgr  29517  isushgr  29518  isupgr  29541  isumgr  29552  isuspgr  29612  isusgr  29613  ushgredgedg  29689  ushgredgedgloop  29691  lfuhgr1v0e  29714  issubgr  29731  subgruhgredgd  29744  subumgredg2  29745  vtxdgfval  29927  vtxdlfgrval  29945  vtxdginducedm1lem2  30000  vtxdginducedm1fi  30004  finsumvtxdg2ssteplem4  30008  finsumvtxdg2size  30010  wlk2v2elem1  30635  dfhnorm2  31603  hlimcaui  31717  hhshsslem1  31748  dmadjss  32368  adjeu  32370  adj1o  32375  gsummpt2co  33488  cycpmrn  33583  tocyccntz  33584  extdgfialglem1  34202  prsdm  34424  mbfmcst  34770  eulerpartlemt  34882  0rrv  34962  coinflipspace  34992  bnj96  35374  bnj1398  35543  bnj1416  35548  bnj1450  35559  bnj1498  35570  bnj1501  35576  fineqvnttrclse  35650  fmla  35960  fmla0  35961  gonan0  35971  satffunlem2lem2  35985  fixun  36486  linedegen  36723  ssbnd  38538  ismgmOLD  38600  exidreslem  38627  n0el2  39083  dmxrn  39135  dmxrncnvepres  39180  dfsucmap2  39212  dmcoss3  39291  dmcoels  39295  dmmzp  43578  cnvrcl0  44465  dvsid  45155  dvsef  45156  modelaxreplem2  45802  dvsinax  46741  fperdvper  46747  dvcosax  46754  stoweidlem27  46855  fourierdlem57  46991  fourierdlem58  46992  fourierdlem62  46996  fourierdlem80  47014  fourierdlem94  47028  fourierdlem97  47031  fourierdlem113  47047  fouriersw  47059  fouriercn  47060  subsaliuncllem  47185  0ome  47357  hoi2toco  47435  isgrim  48798  usgrexmpl1lem  48937  usgrexmpl2lem  48942  gpgprismgr4cycllem8  49018  elbigofrcl  49480  dmtposss  49802  initocmd  50595  termolmd  50596