Theorem dmeqi 5894

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

Syntax hints:   = wceq 1533  dom cdm 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-br 5139  df-dm 5676

This theorem is referenced by:  dmxp  5918  dmxpin  5920  rncoss  5961  rncoeq  5964  rnun  6135  rnin  6136  rnxp  6159  rnxpss  6161  imainrect  6170  dmpropg  6204  dmtpop  6207  rnsnopg  6210  fntpg  6598  opabiotadm  6963  dffv2  6976  fvopab4ndm  7017  fnreseql  7039  dmoprab  7502  reldmmpo  7535  mpondm0  7640  elmpocl  7641  opabn1stprc  8037  bropopvvv  8070  bropfvvvv  8072  frrlem7  8272  frrlem14  8279  wfrdmssOLD  8310  wfrdmclOLD  8312  wfrlem16OLD  8319  tfrlem8  8379  tfr1a  8389  tfr2a  8390  tfr2b  8391  rdgseg  8417  xpassen  9062  sbthlem5  9083  hartogslem1  9533  dmttrcl  9712  r1funlim  9757  r1sucg  9760  r1limg  9762  rankf  9785  hsmexlem4  10420  axdc2lem  10439  dmaddpi  10881  dmmulpi  10882  dmaddsr  11076  dmmulsr  11077  axaddf  11136  axmulf  11137  divsfval  17492  mvdco  19355  symgsssg  19377  symgfisg  19378  pmtrdifellem2  19387  psgnunilem5  19404  ismbl  25377  volres  25379  efcvx  26303  dvrelog  26487  dvlog  26501  nosupcbv  27551  noinfcbv  27566  noetasuplem4  27585  noetainflem4  27589  dmscut  27660  structiedg0val  28751  snstriedgval  28767  isuhgr  28789  isushgr  28790  isupgr  28813  isumgr  28824  isuspgr  28881  isusgr  28882  ushgredgedg  28955  ushgredgedgloop  28957  lfuhgr1v0e  28980  issubgr  28997  subgruhgredgd  29010  subumgredg2  29011  vtxdgfval  29193  vtxdlfgrval  29211  vtxdginducedm1lem2  29266  vtxdginducedm1fi  29270  finsumvtxdg2ssteplem4  29274  finsumvtxdg2size  29276  wlk2v2elem1  29877  dfhnorm2  30844  hlimcaui  30958  hhshsslem1  30989  dmadjss  31609  adjeu  31611  adj1o  31616  gsummpt2co  32668  cycpmrn  32770  tocyccntz  32771  prsdm  33383  mbfmcst  33747  eulerpartlemt  33859  0rrv  33939  coinflipspace  33968  bnj96  34365  bnj1398  34534  bnj1416  34539  bnj1450  34550  bnj1498  34561  bnj1501  34567  fmla  34861  fmla0  34862  gonan0  34872  satffunlem2lem2  34886  fixun  35376  linedegen  35610  matunitlindf  36976  ssbnd  37146  ismgmOLD  37208  exidreslem  37235  n0el2  37692  dmcoss3  37813  dmcoels  37817  dmmzp  41960  cnvrcl0  42865  dvsid  43579  dvsef  43580  dvsinax  45114  fperdvper  45120  dvcosax  45127  stoweidlem27  45228  fourierdlem57  45364  fourierdlem58  45365  fourierdlem62  45369  fourierdlem80  45387  fourierdlem94  45401  fourierdlem97  45404  fourierdlem113  45420  fouriersw  45432  fouriercn  45433  subsaliuncllem  45558  0ome  45730  hoi2toco  45808  elbigofrcl  47424