Theorem dmeqi 5898

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-dm 5668

This theorem is used by:  dmxpin  5925  rncoss  5971  rncoeq  5977  rnun  6154  rninOLD  6156  rnxp  6180  rnxpss  6182  imainrect  6191  dmpropg  6235  dmtpop  6238  rnsnopg  6241  fntpg  6630  opabiotadm  6997  dffv2  7011  fvopab4ndm  7055  fnreseql  7078  dmoprab  7554  reldmmpo  7584  mpondm0  7693  elmpocl  7694  opabn1stprc  8104  bropopvvv  8136  bropfvvvv  8138  frrlem7  8348  frrlem14  8355  tfrlem8  8430  tfr1a  8440  tfr2a  8441  tfr2b  8442  rdgseg  8468  xpassen  9128  sbthlem5  9148  hartogslem1  9573  dmttrcl  9759  r1funlimOLD  9807  r1dmlim  9809  r1sucg  9813  r1limg  9815  rankf  9839  hsmexlem4  10546  axdc2lem  10565  dmaddpi  11014  dmmulpi  11015  dmaddsr  11209  dmmulsr  11210  axaddf  11269  axmulf  11270  divsfval  17769  mgmn0plusgf  18877  degenmgmopdm  19184  degenmgm2opdm  19188  mvdco  19710  symgsssg  19732  symgfisg  19733  pmtrdifellem2  19742  psgnunilem5  19759  matunitlindf  23051  ismbl  25902  volres  25904  efcvx  26833  dvrelog  27022  dvlog  27036  nosupcbv  28116  noinfcbv  28131  noetasuplem4  28150  noetainflem4  28154  dmcuts  28234  structiedg0val  29657  snstriedgval  29673  isuhgr  29695  isushgr  29696  isupgr  29719  isumgr  29730  isuspgr  29790  isusgr  29791  ushgredgedg  29867  ushgredgedgloop  29869  lfuhgr1v0e  29892  issubgr  29909  subgruhgredgd  29922  subumgredg2  29923  vtxdgfval  30105  vtxdlfgrval  30123  vtxdginducedm1lem2  30178  vtxdginducedm1fi  30182  finsumvtxdg2ssteplem4  30186  finsumvtxdg2size  30188  wlk2v2elem1  30813  dfhnorm2  31781  hlimcaui  31895  hhshsslem1  31926  dmadjss  32546  adjeu  32548  adj1o  32553  gsummpt2co  33708  cycpmrn  33803  tocyccntz  33804  extdgfialglem1  34435  prsdm  34657  mbfmcst  35002  eulerpartlemt  35114  0rrv  35194  coinflipspace  35224  bnj96  35606  bnj1398  35775  bnj1416  35780  bnj1450  35791  bnj1498  35802  bnj1501  35808  fwfffunres  35829  fineqvnttrclse  35933  dmr0ss  36043  fmla  36354  fmla0  36355  gonan0  36365  satffunlem2lem2  36379  fixun  36886  linedegen  37123  ssbnd  38988  ismgmOLD  39050  exidreslem  39077  n0el2  39533  dmxrn  39585  dmxrncnvepres  39630  dfsucmap2  39662  dmcoss3  39741  dmcoels  39745  dmmzp  44010  cnvrcl0  44886  dvsid  45576  dvsef  45577  modelaxreplem2  46233  dvsinax  47196  fperdvper  47202  dvcosax  47209  stoweidlem27  47310  fourierdlem57  47446  fourierdlem58  47447  fourierdlem62  47451  fourierdlem80  47469  fourierdlem94  47483  fourierdlem97  47486  fourierdlem113  47502  fouriersw  47514  fouriercn  47515  subsaliuncllem  47640  0ome  47812  hoi2toco  47890  isgrim  49253  usgrexmpl1lem  49392  usgrexmpl2lem  49397  gpgprismgr4cycllem8  49473  elbigofrcl  49993  dmtposss  50320  initocmd  51183  termolmd  51184