Theorem dmeqi 5861

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

Syntax hints:   = wceq 1542  dom cdm 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-dm 5642

This theorem is referenced by:  dmxpin  5888  rncoss  5934  rncoeq  5939  rnun  6111  rnin  6112  rnxp  6136  rnxpss  6138  imainrect  6147  dmpropg  6181  dmtpop  6184  rnsnopg  6187  fntpg  6560  opabiotadm  6923  dffv2  6937  fvopab4ndm  6980  fnreseql  7002  dmoprab  7471  reldmmpo  7502  mpondm0  7608  elmpocl  7609  opabn1stprc  8012  bropopvvv  8042  bropfvvvv  8044  frrlem7  8244  frrlem14  8251  tfrlem8  8325  tfr1a  8335  tfr2a  8336  tfr2b  8337  rdgseg  8363  xpassen  9011  sbthlem5  9031  hartogslem1  9459  dmttrcl  9642  r1funlim  9690  r1sucg  9693  r1limg  9695  rankf  9718  hsmexlem4  10351  axdc2lem  10370  dmaddpi  10813  dmmulpi  10814  dmaddsr  11008  dmmulsr  11009  axaddf  11068  axmulf  11069  divsfval  17480  mvdco  19386  symgsssg  19408  symgfisg  19409  pmtrdifellem2  19418  psgnunilem5  19435  ismbl  25495  volres  25497  efcvx  26427  dvrelog  26614  dvlog  26628  nosupcbv  27682  noinfcbv  27697  noetasuplem4  27716  noetainflem4  27720  dmcuts  27799  structiedg0val  29107  snstriedgval  29123  isuhgr  29145  isushgr  29146  isupgr  29169  isumgr  29180  isuspgr  29237  isusgr  29238  ushgredgedg  29314  ushgredgedgloop  29316  lfuhgr1v0e  29339  issubgr  29356  subgruhgredgd  29369  subumgredg2  29370  vtxdgfval  29553  vtxdlfgrval  29571  vtxdginducedm1lem2  29626  vtxdginducedm1fi  29630  finsumvtxdg2ssteplem4  29634  finsumvtxdg2size  29636  wlk2v2elem1  30242  dfhnorm2  31210  hlimcaui  31324  hhshsslem1  31355  dmadjss  31975  adjeu  31977  adj1o  31982  gsummpt2co  33142  cycpmrn  33237  tocyccntz  33238  extdgfialglem1  33870  prsdm  34092  mbfmcst  34437  eulerpartlemt  34549  0rrv  34629  coinflipspace  34659  bnj96  35041  bnj1398  35210  bnj1416  35215  bnj1450  35226  bnj1498  35237  bnj1501  35243  fineqvnttrclse  35302  fmla  35597  fmla0  35598  gonan0  35608  satffunlem2lem2  35622  fixun  36123  linedegen  36359  matunitlindf  37869  ssbnd  38039  ismgmOLD  38101  exidreslem  38128  n0el2  38586  dmxrn  38638  dmxrncnvepres  38683  dfsucmap2  38715  dmcoss3  38794  dmcoels  38798  dmmzp  43090  cnvrcl0  43981  dvsid  44687  dvsef  44688  modelaxreplem2  45335  dvsinax  46271  fperdvper  46277  dvcosax  46284  stoweidlem27  46385  fourierdlem57  46521  fourierdlem58  46522  fourierdlem62  46526  fourierdlem80  46544  fourierdlem94  46558  fourierdlem97  46561  fourierdlem113  46577  fouriersw  46589  fouriercn  46590  subsaliuncllem  46715  0ome  46887  hoi2toco  46965  isgrim  48242  usgrexmpl1lem  48381  usgrexmpl2lem  48386  gpgprismgr4cycllem8  48462  elbigofrcl  48910  dmtposss  49235  initocmd  50028  termolmd  50029