Theorem dmeqi 5871

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

Syntax hints:   = wceq 1540  dom cdm 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-dm 5651

This theorem is referenced by:  dmxpOLD  5896  dmxpin  5898  rncoss  5942  rncoeq  5946  rnun  6121  rnin  6122  rnxp  6146  rnxpss  6148  imainrect  6157  dmpropg  6191  dmtpop  6194  rnsnopg  6197  fntpg  6579  opabiotadm  6945  dffv2  6959  fvopab4ndm  7001  fnreseql  7023  dmoprab  7495  reldmmpo  7526  mpondm0  7632  elmpocl  7633  opabn1stprc  8040  bropopvvv  8072  bropfvvvv  8074  frrlem7  8274  frrlem14  8281  tfrlem8  8355  tfr1a  8365  tfr2a  8366  tfr2b  8367  rdgseg  8393  xpassen  9040  sbthlem5  9061  hartogslem1  9502  dmttrcl  9681  r1funlim  9726  r1sucg  9729  r1limg  9731  rankf  9754  hsmexlem4  10389  axdc2lem  10408  dmaddpi  10850  dmmulpi  10851  dmaddsr  11045  dmmulsr  11046  axaddf  11105  axmulf  11106  divsfval  17517  mvdco  19382  symgsssg  19404  symgfisg  19405  pmtrdifellem2  19414  psgnunilem5  19431  ismbl  25434  volres  25436  efcvx  26366  dvrelog  26553  dvlog  26567  nosupcbv  27621  noinfcbv  27636  noetasuplem4  27655  noetainflem4  27659  dmscut  27730  structiedg0val  28956  snstriedgval  28972  isuhgr  28994  isushgr  28995  isupgr  29018  isumgr  29029  isuspgr  29086  isusgr  29087  ushgredgedg  29163  ushgredgedgloop  29165  lfuhgr1v0e  29188  issubgr  29205  subgruhgredgd  29218  subumgredg2  29219  vtxdgfval  29402  vtxdlfgrval  29420  vtxdginducedm1lem2  29475  vtxdginducedm1fi  29479  finsumvtxdg2ssteplem4  29483  finsumvtxdg2size  29485  wlk2v2elem1  30091  dfhnorm2  31058  hlimcaui  31172  hhshsslem1  31203  dmadjss  31823  adjeu  31825  adj1o  31830  gsummpt2co  32995  cycpmrn  33107  tocyccntz  33108  prsdm  33911  mbfmcst  34257  eulerpartlemt  34369  0rrv  34449  coinflipspace  34479  bnj96  34862  bnj1398  35031  bnj1416  35036  bnj1450  35047  bnj1498  35058  bnj1501  35064  fmla  35375  fmla0  35376  gonan0  35386  satffunlem2lem2  35400  fixun  35904  linedegen  36138  matunitlindf  37619  ssbnd  37789  ismgmOLD  37851  exidreslem  37878  n0el2  38324  dmxrn  38367  dmxrncnvepres  38402  dmcoss3  38451  dmcoels  38455  dmmzp  42728  cnvrcl0  43621  dvsid  44327  dvsef  44328  modelaxreplem2  44976  dvsinax  45918  fperdvper  45924  dvcosax  45931  stoweidlem27  46032  fourierdlem57  46168  fourierdlem58  46169  fourierdlem62  46173  fourierdlem80  46191  fourierdlem94  46205  fourierdlem97  46208  fourierdlem113  46224  fouriersw  46236  fouriercn  46237  subsaliuncllem  46362  0ome  46534  hoi2toco  46612  isgrim  47886  usgrexmpl1lem  48016  usgrexmpl2lem  48021  gpgprismgr4cycllem8  48096  elbigofrcl  48543  dmtposss  48868  initocmd  49662  termolmd  49663