Theorem dmeqi 5247

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

Syntax hints:   = wceq 1475  dom cdm 5038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-dm 5048

This theorem is referenced by:  dmxp  5265  dmxpin  5267  rncoss  5307  rncoeq  5310  rnun  5460  rnin  5461  rnxp  5483  rnxpss  5485  imainrect  5494  dmpropg  5526  dmtpop  5529  rnsnopg  5532  fntpg  5862  opabiotadm  6170  dffv2  6181  fvopab4ndm  6215  fnreseql  6235  dmoprab  6639  reldmmpt2  6669  mpt2ndm0  6773  elmpt2cl  6774  bropopvvv  7142  bropfvvvv  7144  wfrdmss  7308  wfrdmcl  7310  wfrlem16  7317  tfrlem8  7367  tfr1a  7377  tfr2a  7378  tfr2b  7379  rdgseg  7405  xpassen  7939  sbthlem5  7959  hartogslem1  8330  r1funlim  8512  r1sucg  8515  r1limg  8517  rankf  8540  hsmexlem4  9134  axdc2lem  9153  dmaddpi  9591  dmmulpi  9592  dmaddsr  9785  dmmulsr  9786  axaddf  9845  axmulf  9846  strlemor1  15796  divsfval  16030  xpsfrnel2  16048  mvdco  17688  symgsssg  17710  symgfisg  17711  pmtrdifellem2  17720  psgnunilem5  17737  ismbl  23101  volres  23103  efcvx  24007  dvrelog  24183  dvlog  24197  structiedg0val  25699  snstriedgval  25713  isuhgr  25726  isushgr  25727  isupgr  25751  isumgr  25761  usgrares1  25939  usgrafilem1  25940  cusgrasizeindslem1  26002  wlkntrllem1  26089  clwwlknprop  26300  2wlkonot3v  26402  2spthonot3v  26403  eupares  26502  dfhnorm2  27363  hlimcaui  27477  hhshsslem1  27508  dmadjss  28130  adjeu  28132  adj1o  28137  gsummpt2co  29111  prsdm  29288  mbfmcst  29648  eulerpartlemt  29760  0rrv  29840  coinflipspace  29869  bnj96  30189  bnj1398  30356  bnj1416  30361  bnj1450  30372  bnj1498  30383  bnj1501  30389  frrlem7  31034  nofulllem5  31105  fixun  31186  linedegen  31420  matunitlindf  32577  ssbnd  32757  ismgmOLD  32819  exidreslem  32846  dmmzp  36314  cnvrcl0  36951  dvsid  37552  dvsef  37553  dvsinax  38801  fperdvper  38808  dvcosax  38816  stoweidlem27  38920  fourierdlem57  39056  fourierdlem58  39057  fourierdlem62  39061  fourierdlem80  39079  fourierdlem94  39093  fourierdlem97  39096  fourierdlem113  39112  fouriersw  39124  fouriercn  39125  subsaliuncllem  39251  0ome  39419  hoi2toco  39497  opabn1stprc  40318  isuspgr  40382  isusgr  40383  ushgredgedga  40456  ushgredgedgaloop  40458  lfuhgr1v0e  40480  issubgr  40495  subgruhgredgd  40508  subumgredg2  40509  vtxdgfval  40683  vtxdlfgrval  40700  1wlk2v2elem1  41322  1wlk2v2elem2  41323  elbigofrcl  42142