Theorem dmeqi 5886

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

This proof depends on syntax axioms:   = wceq 1569  dom cdm 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-dm 5660

This theorem is used by:  dmxpin  5913  rncoss  5959  rncoeq  5963  rnun  6137  rninOLD  6139  rnxp  6163  rnxpss  6165  imainrect  6174  dmpropg  6218  dmtpop  6221  rnsnopg  6224  fntpg  6603  opabiotadm  6969  dffv2  6983  fvopab4ndm  7027  fnreseql  7050  dmoprab  7525  reldmmpo  7556  mpondm0  7663  elmpocl  7664  opabn1stprc  8071  bropopvvv  8103  bropfvvvv  8105  frrlem7  8315  frrlem14  8322  tfrlem8  8397  tfr1a  8407  tfr2a  8408  tfr2b  8409  rdgseg  8435  xpassen  9095  sbthlem5  9115  hartogslem1  9541  dmttrcl  9727  r1funlimOLD  9775  r1dmlim  9777  r1sucg  9781  r1limg  9783  rankf  9807  hsmexlem4  10512  axdc2lem  10531  dmaddpi  10980  dmmulpi  10981  dmaddsr  11175  dmmulsr  11176  axaddf  11235  axmulf  11236  divsfval  17726  mgmn0plusgf  18834  degenmgmopdm  19141  degenmgm2opdm  19145  mvdco  19666  symgsssg  19688  symgfisg  19689  pmtrdifellem2  19698  psgnunilem5  19715  matunitlindf  23003  ismbl  25854  volres  25856  efcvx  26783  dvrelog  26972  dvlog  26986  nosupcbv  28066  noinfcbv  28081  noetasuplem4  28100  noetainflem4  28104  dmcuts  28184  structiedg0val  29607  snstriedgval  29623  isuhgr  29645  isushgr  29646  isupgr  29669  isumgr  29680  isuspgr  29740  isusgr  29741  ushgredgedg  29817  ushgredgedgloop  29819  lfuhgr1v0e  29842  issubgr  29859  subgruhgredgd  29872  subumgredg2  29873  vtxdgfval  30055  vtxdlfgrval  30073  vtxdginducedm1lem2  30128  vtxdginducedm1fi  30132  finsumvtxdg2ssteplem4  30136  finsumvtxdg2size  30138  wlk2v2elem1  30763  dfhnorm2  31731  hlimcaui  31845  hhshsslem1  31876  dmadjss  32496  adjeu  32498  adj1o  32503  gsummpt2co  33657  cycpmrn  33752  tocyccntz  33753  extdgfialglem1  34372  prsdm  34594  mbfmcst  34939  eulerpartlemt  35051  0rrv  35131  coinflipspace  35161  bnj96  35543  bnj1398  35712  bnj1416  35717  bnj1450  35728  bnj1498  35739  bnj1501  35745  fwfffunres  35766  fineqvnttrclse  35850  dmr0ss  35943  fmla  36234  fmla0  36235  gonan0  36245  satffunlem2lem2  36259  fixun  36765  linedegen  37002  ssbnd  38829  ismgmOLD  38891  exidreslem  38918  n0el2  39374  dmxrn  39426  dmxrncnvepres  39471  dfsucmap2  39503  dmcoss3  39582  dmcoels  39586  dmmzp  43851  cnvrcl0  44732  dvsid  45422  dvsef  45423  modelaxreplem2  46076  dvsinax  47030  fperdvper  47036  dvcosax  47043  stoweidlem27  47144  fourierdlem57  47280  fourierdlem58  47281  fourierdlem62  47285  fourierdlem80  47303  fourierdlem94  47317  fourierdlem97  47320  fourierdlem113  47336  fouriersw  47348  fouriercn  47349  subsaliuncllem  47474  0ome  47646  hoi2toco  47724  isgrim  49087  usgrexmpl1lem  49226  usgrexmpl2lem  49231  gpgprismgr4cycllem8  49307  elbigofrcl  49769  dmtposss  50096  initocmd  50959  termolmd  50960