Theorem dmeqi 5892

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

Syntax hints:   = wceq 1567  dom cdm 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-dm 5669

This theorem is referenced by:  dmxpin  5919  rncoss  5965  rncoeq  5969  rnun  6140  rninOLD  6142  rnxp  6166  rnxpss  6168  imainrect  6177  dmpropg  6214  dmtpop  6217  rnsnopg  6220  fntpg  6594  opabiotadm  6960  dffv2  6974  fvopab4ndm  7018  fnreseql  7041  dmoprab  7511  reldmmpo  7542  mpondm0  7648  elmpocl  7649  opabn1stprc  8051  bropopvvv  8081  bropfvvvv  8083  frrlem7  8285  frrlem14  8292  tfrlem8  8367  tfr1a  8377  tfr2a  8378  tfr2b  8379  rdgseg  8405  xpassen  9055  sbthlem5  9075  hartogslem1  9500  dmttrcl  9686  r1funlim  9734  r1sucg  9737  r1limg  9739  rankf  9762  hsmexlem4  10409  axdc2lem  10428  dmaddpi  10871  dmmulpi  10872  dmaddsr  11066  dmmulsr  11067  axaddf  11126  axmulf  11127  divsfval  17597  mvdco  19511  symgsssg  19533  symgfisg  19534  pmtrdifellem2  19543  psgnunilem5  19560  ismbl  25650  volres  25652  efcvx  26574  dvrelog  26764  dvlog  26778  nosupcbv  27828  noinfcbv  27843  noetasuplem4  27862  noetainflem4  27866  dmcuts  27946  structiedg0val  29309  snstriedgval  29325  isuhgr  29347  isushgr  29348  isupgr  29371  isumgr  29382  isuspgr  29439  isusgr  29440  ushgredgedg  29516  ushgredgedgloop  29518  lfuhgr1v0e  29541  issubgr  29558  subgruhgredgd  29571  subumgredg2  29572  vtxdgfval  29754  vtxdlfgrval  29772  vtxdginducedm1lem2  29827  vtxdginducedm1fi  29831  finsumvtxdg2ssteplem4  29835  finsumvtxdg2size  29837  wlk2v2elem1  30443  dfhnorm2  31411  hlimcaui  31525  hhshsslem1  31556  dmadjss  32176  adjeu  32178  adj1o  32183  gsummpt2co  33305  cycpmrn  33400  tocyccntz  33401  extdgfialglem1  34023  prsdm  34245  mbfmcst  34590  eulerpartlemt  34702  0rrv  34782  coinflipspace  34812  bnj96  35194  bnj1398  35363  bnj1416  35368  bnj1450  35379  bnj1498  35390  bnj1501  35396  fineqvnttrclse  35456  fmla  35768  fmla0  35769  gonan0  35779  satffunlem2lem2  35793  fixun  36294  linedegen  36530  matunitlindf  38152  ssbnd  38322  ismgmOLD  38384  exidreslem  38411  n0el2  38869  dmxrn  38921  dmxrncnvepres  38966  dfsucmap2  38998  dmcoss3  39077  dmcoels  39081  dmmzp  43351  cnvrcl0  44238  dvsid  44928  dvsef  44929  modelaxreplem2  45575  dvsinax  46514  fperdvper  46520  dvcosax  46527  stoweidlem27  46628  fourierdlem57  46764  fourierdlem58  46765  fourierdlem62  46769  fourierdlem80  46787  fourierdlem94  46801  fourierdlem97  46804  fourierdlem113  46820  fouriersw  46832  fouriercn  46833  subsaliuncllem  46958  0ome  47130  hoi2toco  47208  isgrim  48531  usgrexmpl1lem  48670  usgrexmpl2lem  48675  gpgprismgr4cycllem8  48751  elbigofrcl  49210  dmtposss  49534  initocmd  50327  termolmd  50328