Theorem dmeqi 5737

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

Syntax hints:   = wceq 1538  dom cdm 5519

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-dm 5529

This theorem is referenced by:  dmxp  5763  dmxpin  5765  rncoss  5808  rncoeq  5811  rnun  5971  rnin  5972  rnxp  5994  rnxpss  5996  imainrect  6005  dmpropg  6039  dmtpop  6042  rnsnopg  6045  fntpg  6384  opabiotadm  6720  dffv2  6733  fvopab4ndm  6774  fnreseql  6795  dmoprab  7234  reldmmpo  7264  mpondm0  7366  elmpocl  7367  opabn1stprc  7738  bropopvvv  7768  bropfvvvv  7770  wfrdmss  7944  wfrdmcl  7946  wfrlem16  7953  tfrlem8  8003  tfr1a  8013  tfr2a  8014  tfr2b  8015  rdgseg  8041  xpassen  8594  sbthlem5  8615  hartogslem1  8990  r1funlim  9179  r1sucg  9182  r1limg  9184  rankf  9207  hsmexlem4  9840  axdc2lem  9859  dmaddpi  10301  dmmulpi  10302  dmaddsr  10496  dmmulsr  10497  axaddf  10556  axmulf  10557  divsfval  16812  mvdco  18565  symgsssg  18587  symgfisg  18588  pmtrdifellem2  18597  psgnunilem5  18614  ismbl  24130  volres  24132  efcvx  25044  dvrelog  25228  dvlog  25242  structiedg0val  26815  snstriedgval  26831  isuhgr  26853  isushgr  26854  isupgr  26877  isumgr  26888  isuspgr  26945  isusgr  26946  ushgredgedg  27019  ushgredgedgloop  27021  lfuhgr1v0e  27044  issubgr  27061  subgruhgredgd  27074  subumgredg2  27075  vtxdgfval  27257  vtxdlfgrval  27275  vtxdginducedm1lem2  27330  vtxdginducedm1fi  27334  finsumvtxdg2ssteplem4  27338  finsumvtxdg2size  27340  wlk2v2elem1  27940  dfhnorm2  28905  hlimcaui  29019  hhshsslem1  29050  dmadjss  29670  adjeu  29672  adj1o  29677  gsummpt2co  30733  cycpmrn  30835  tocyccntz  30836  prsdm  31267  mbfmcst  31627  eulerpartlemt  31739  0rrv  31819  coinflipspace  31848  bnj96  32247  bnj1398  32416  bnj1416  32421  bnj1450  32432  bnj1498  32443  bnj1501  32449  fmla  32741  fmla0  32742  gonan0  32752  satffunlem2lem2  32766  frrlem7  33242  frrlem14  33249  noetalem3  33332  noetalem4  33333  dmscut  33385  fixun  33483  linedegen  33717  matunitlindf  35055  ssbnd  35226  ismgmOLD  35288  exidreslem  35315  n0el2  35750  dmcoss3  35853  dmcoels  35857  dmmzp  39674  cnvrcl0  40325  dvsid  41035  dvsef  41036  dvsinax  42555  fperdvper  42561  dvcosax  42568  stoweidlem27  42669  fourierdlem57  42805  fourierdlem58  42806  fourierdlem62  42810  fourierdlem80  42828  fourierdlem94  42842  fourierdlem97  42845  fourierdlem113  42861  fouriersw  42873  fouriercn  42874  subsaliuncllem  42997  0ome  43168  hoi2toco  43246  elbigofrcl  44964