Theorem dmeqi 5850

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

Syntax hints:   = wceq 1541  dom cdm 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-dm 5631

This theorem is referenced by:  dmxpin  5877  rncoss  5923  rncoeq  5928  rnun  6100  rnin  6101  rnxp  6125  rnxpss  6127  imainrect  6136  dmpropg  6170  dmtpop  6173  rnsnopg  6176  fntpg  6549  opabiotadm  6912  dffv2  6926  fvopab4ndm  6968  fnreseql  6990  dmoprab  7458  reldmmpo  7489  mpondm0  7595  elmpocl  7596  opabn1stprc  7999  bropopvvv  8029  bropfvvvv  8031  frrlem7  8231  frrlem14  8238  tfrlem8  8312  tfr1a  8322  tfr2a  8323  tfr2b  8324  rdgseg  8350  xpassen  8995  sbthlem5  9015  hartogslem1  9439  dmttrcl  9622  r1funlim  9670  r1sucg  9673  r1limg  9675  rankf  9698  hsmexlem4  10331  axdc2lem  10350  dmaddpi  10792  dmmulpi  10793  dmaddsr  10987  dmmulsr  10988  axaddf  11047  axmulf  11048  divsfval  17459  mvdco  19365  symgsssg  19387  symgfisg  19388  pmtrdifellem2  19397  psgnunilem5  19414  ismbl  25474  volres  25476  efcvx  26406  dvrelog  26593  dvlog  26607  nosupcbv  27661  noinfcbv  27676  noetasuplem4  27695  noetainflem4  27699  dmscut  27772  structiedg0val  29021  snstriedgval  29037  isuhgr  29059  isushgr  29060  isupgr  29083  isumgr  29094  isuspgr  29151  isusgr  29152  ushgredgedg  29228  ushgredgedgloop  29230  lfuhgr1v0e  29253  issubgr  29270  subgruhgredgd  29283  subumgredg2  29284  vtxdgfval  29467  vtxdlfgrval  29485  vtxdginducedm1lem2  29540  vtxdginducedm1fi  29544  finsumvtxdg2ssteplem4  29548  finsumvtxdg2size  29550  wlk2v2elem1  30156  dfhnorm2  31123  hlimcaui  31237  hhshsslem1  31268  dmadjss  31888  adjeu  31890  adj1o  31895  gsummpt2co  33059  cycpmrn  33153  tocyccntz  33154  extdgfialglem1  33777  prsdm  33999  mbfmcst  34344  eulerpartlemt  34456  0rrv  34536  coinflipspace  34566  bnj96  34949  bnj1398  35118  bnj1416  35123  bnj1450  35134  bnj1498  35145  bnj1501  35151  fineqvnttrclse  35216  fmla  35497  fmla0  35498  gonan0  35508  satffunlem2lem2  35522  fixun  36023  linedegen  36259  matunitlindf  37731  ssbnd  37901  ismgmOLD  37963  exidreslem  37990  n0el2  38440  dmxrn  38484  dmxrncnvepres  38529  dfsucmap2  38550  dmcoss3  38628  dmcoels  38632  dmmzp  42890  cnvrcl0  43782  dvsid  44488  dvsef  44489  modelaxreplem2  45136  dvsinax  46073  fperdvper  46079  dvcosax  46086  stoweidlem27  46187  fourierdlem57  46323  fourierdlem58  46324  fourierdlem62  46328  fourierdlem80  46346  fourierdlem94  46360  fourierdlem97  46363  fourierdlem113  46379  fouriersw  46391  fouriercn  46392  subsaliuncllem  46517  0ome  46689  hoi2toco  46767  isgrim  48044  usgrexmpl1lem  48183  usgrexmpl2lem  48188  gpgprismgr4cycllem8  48264  elbigofrcl  48712  dmtposss  49037  initocmd  49830  termolmd  49831