Theorem dmeqi 5884

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

Syntax hints:   = wceq 1540  dom cdm 5654

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-dm 5664

This theorem is referenced by:  dmxpOLD  5909  dmxpin  5911  rncoss  5955  rncoeq  5959  rnun  6134  rnin  6135  rnxp  6159  rnxpss  6161  imainrect  6170  dmpropg  6204  dmtpop  6207  rnsnopg  6210  fntpg  6596  opabiotadm  6960  dffv2  6974  fvopab4ndm  7016  fnreseql  7038  dmoprab  7510  reldmmpo  7541  mpondm0  7647  elmpocl  7648  opabn1stprc  8057  bropopvvv  8089  bropfvvvv  8091  frrlem7  8291  frrlem14  8298  wfrdmssOLD  8329  wfrdmclOLD  8331  wfrlem16OLD  8338  tfrlem8  8398  tfr1a  8408  tfr2a  8409  tfr2b  8410  rdgseg  8436  xpassen  9080  sbthlem5  9101  hartogslem1  9556  dmttrcl  9735  r1funlim  9780  r1sucg  9783  r1limg  9785  rankf  9808  hsmexlem4  10443  axdc2lem  10462  dmaddpi  10904  dmmulpi  10905  dmaddsr  11099  dmmulsr  11100  axaddf  11159  axmulf  11160  divsfval  17561  mvdco  19426  symgsssg  19448  symgfisg  19449  pmtrdifellem2  19458  psgnunilem5  19475  ismbl  25479  volres  25481  efcvx  26411  dvrelog  26598  dvlog  26612  nosupcbv  27666  noinfcbv  27681  noetasuplem4  27700  noetainflem4  27704  dmscut  27775  structiedg0val  29001  snstriedgval  29017  isuhgr  29039  isushgr  29040  isupgr  29063  isumgr  29074  isuspgr  29131  isusgr  29132  ushgredgedg  29208  ushgredgedgloop  29210  lfuhgr1v0e  29233  issubgr  29250  subgruhgredgd  29263  subumgredg2  29264  vtxdgfval  29447  vtxdlfgrval  29465  vtxdginducedm1lem2  29520  vtxdginducedm1fi  29524  finsumvtxdg2ssteplem4  29528  finsumvtxdg2size  29530  wlk2v2elem1  30136  dfhnorm2  31103  hlimcaui  31217  hhshsslem1  31248  dmadjss  31868  adjeu  31870  adj1o  31875  gsummpt2co  33042  cycpmrn  33154  tocyccntz  33155  prsdm  33945  mbfmcst  34291  eulerpartlemt  34403  0rrv  34483  coinflipspace  34513  bnj96  34896  bnj1398  35065  bnj1416  35070  bnj1450  35081  bnj1498  35092  bnj1501  35098  fmla  35403  fmla0  35404  gonan0  35414  satffunlem2lem2  35428  fixun  35927  linedegen  36161  matunitlindf  37642  ssbnd  37812  ismgmOLD  37874  exidreslem  37901  n0el2  38351  dmcoss3  38471  dmcoels  38475  dmmzp  42756  cnvrcl0  43649  dvsid  44355  dvsef  44356  modelaxreplem2  45004  dvsinax  45942  fperdvper  45948  dvcosax  45955  stoweidlem27  46056  fourierdlem57  46192  fourierdlem58  46193  fourierdlem62  46197  fourierdlem80  46215  fourierdlem94  46229  fourierdlem97  46232  fourierdlem113  46248  fouriersw  46260  fouriercn  46261  subsaliuncllem  46386  0ome  46558  hoi2toco  46636  isgrim  47895  usgrexmpl1lem  48025  usgrexmpl2lem  48030  gpgprismgr4cycllem8  48101  elbigofrcl  48530  dmtposss  48851