Theorem dmeqi 5747

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

Syntax hints:   = wceq 1542  dom cdm 5525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-un 3848  df-in 3850  df-ss 3860  df-sn 4517  df-pr 4519  df-op 4523  df-br 5031  df-dm 5535

This theorem is referenced by:  dmxp  5772  dmxpin  5774  rncoss  5815  rncoeq  5818  rnun  5978  rnin  5979  rnxp  6002  rnxpss  6004  imainrect  6013  dmpropg  6047  dmtpop  6050  rnsnopg  6053  fntpg  6399  opabiotadm  6750  dffv2  6763  fvopab4ndm  6804  fnreseql  6825  dmoprab  7269  reldmmpo  7300  mpondm0  7402  elmpocl  7403  opabn1stprc  7781  bropopvvv  7811  bropfvvvv  7813  wfrdmss  7990  wfrdmcl  7992  wfrlem16  7999  tfrlem8  8049  tfr1a  8059  tfr2a  8060  tfr2b  8061  rdgseg  8087  xpassen  8660  sbthlem5  8681  hartogslem1  9079  r1funlim  9268  r1sucg  9271  r1limg  9273  rankf  9296  hsmexlem4  9929  axdc2lem  9948  dmaddpi  10390  dmmulpi  10391  dmaddsr  10585  dmmulsr  10586  axaddf  10645  axmulf  10646  divsfval  16923  mvdco  18691  symgsssg  18713  symgfisg  18714  pmtrdifellem2  18723  psgnunilem5  18740  ismbl  24278  volres  24280  efcvx  25196  dvrelog  25380  dvlog  25394  structiedg0val  26967  snstriedgval  26983  isuhgr  27005  isushgr  27006  isupgr  27029  isumgr  27040  isuspgr  27097  isusgr  27098  ushgredgedg  27171  ushgredgedgloop  27173  lfuhgr1v0e  27196  issubgr  27213  subgruhgredgd  27226  subumgredg2  27227  vtxdgfval  27409  vtxdlfgrval  27427  vtxdginducedm1lem2  27482  vtxdginducedm1fi  27486  finsumvtxdg2ssteplem4  27490  finsumvtxdg2size  27492  wlk2v2elem1  28092  dfhnorm2  29057  hlimcaui  29171  hhshsslem1  29202  dmadjss  29822  adjeu  29824  adj1o  29829  gsummpt2co  30885  cycpmrn  30987  tocyccntz  30988  prsdm  31436  mbfmcst  31796  eulerpartlemt  31908  0rrv  31988  coinflipspace  32017  bnj96  32416  bnj1398  32585  bnj1416  32590  bnj1450  32601  bnj1498  32612  bnj1501  32618  fmla  32914  fmla0  32915  gonan0  32925  satffunlem2lem2  32939  frrlem7  33447  frrlem14  33454  nosupcbv  33546  noinfcbv  33561  noetasuplem4  33580  noetainflem4  33584  dmscut  33646  fixun  33849  linedegen  34083  matunitlindf  35398  ssbnd  35569  ismgmOLD  35631  exidreslem  35658  n0el2  36091  dmcoss3  36194  dmcoels  36198  dmmzp  40127  cnvrcl0  40778  dvsid  41487  dvsef  41488  dvsinax  42996  fperdvper  43002  dvcosax  43009  stoweidlem27  43110  fourierdlem57  43246  fourierdlem58  43247  fourierdlem62  43251  fourierdlem80  43269  fourierdlem94  43283  fourierdlem97  43286  fourierdlem113  43302  fouriersw  43314  fouriercn  43315  subsaliuncllem  43438  0ome  43609  hoi2toco  43687  elbigofrcl  45430