Theorem dmeqi 5896

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

This proof depends on syntax axioms:   = wceq 1570  dom cdm 5663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-dm 5673

This theorem is used by:  dmxpin  5923  rncoss  5969  rncoeq  5973  rnun  6144  rninOLD  6146  rnxp  6170  rnxpss  6172  imainrect  6181  dmpropg  6218  dmtpop  6221  rnsnopg  6224  fntpg  6600  opabiotadm  6966  dffv2  6980  fvopab4ndm  7024  fnreseql  7047  dmoprab  7522  reldmmpo  7553  mpondm0  7660  elmpocl  7661  opabn1stprc  8061  bropopvvv  8091  bropfvvvv  8093  frrlem7  8295  frrlem14  8302  tfrlem8  8377  tfr1a  8387  tfr2a  8388  tfr2b  8389  rdgseg  8415  xpassen  9066  sbthlem5  9086  hartogslem1  9511  dmttrcl  9697  r1funlim  9745  r1sucg  9748  r1limg  9750  rankf  9773  hsmexlem4  10428  axdc2lem  10447  dmaddpi  10890  dmmulpi  10891  dmaddsr  11085  dmmulsr  11086  axaddf  11145  axmulf  11146  divsfval  17623  mgmn0plusgf  18731  degenmgmopdm  19034  degenmgm2opdm  19038  mvdco  19559  symgsssg  19581  symgfisg  19582  pmtrdifellem2  19591  psgnunilem5  19608  ismbl  25736  volres  25738  efcvx  26663  dvrelog  26853  dvlog  26867  nosupcbv  27917  noinfcbv  27932  noetasuplem4  27951  noetainflem4  27955  dmcuts  28035  structiedg0val  29427  snstriedgval  29443  isuhgr  29465  isushgr  29466  isupgr  29489  isumgr  29500  isuspgr  29560  isusgr  29561  ushgredgedg  29637  ushgredgedgloop  29639  lfuhgr1v0e  29662  issubgr  29679  subgruhgredgd  29692  subumgredg2  29693  vtxdgfval  29875  vtxdlfgrval  29893  vtxdginducedm1lem2  29948  vtxdginducedm1fi  29952  finsumvtxdg2ssteplem4  29956  finsumvtxdg2size  29958  wlk2v2elem1  30577  dfhnorm2  31545  hlimcaui  31659  hhshsslem1  31690  dmadjss  32310  adjeu  32312  adj1o  32317  gsummpt2co  33432  cycpmrn  33527  tocyccntz  33528  extdgfialglem1  34146  prsdm  34368  mbfmcst  34714  eulerpartlemt  34826  0rrv  34906  coinflipspace  34936  bnj96  35318  bnj1398  35487  bnj1416  35492  bnj1450  35503  bnj1498  35514  bnj1501  35520  fineqvnttrclse  35594  fmla  35910  fmla0  35911  gonan0  35921  satffunlem2lem2  35935  fixun  36436  linedegen  36672  matunitlindf  38326  ssbnd  38497  ismgmOLD  38559  exidreslem  38586  n0el2  39042  dmxrn  39094  dmxrncnvepres  39139  dfsucmap2  39171  dmcoss3  39250  dmcoels  39254  dmmzp  43522  cnvrcl0  44409  dvsid  45099  dvsef  45100  modelaxreplem2  45746  dvsinax  46685  fperdvper  46691  dvcosax  46698  stoweidlem27  46799  fourierdlem57  46935  fourierdlem58  46936  fourierdlem62  46940  fourierdlem80  46958  fourierdlem94  46972  fourierdlem97  46975  fourierdlem113  46991  fouriersw  47003  fouriercn  47004  subsaliuncllem  47129  0ome  47301  hoi2toco  47379  isgrim  48705  usgrexmpl1lem  48844  usgrexmpl2lem  48849  gpgprismgr4cycllem8  48925  elbigofrcl  49387  dmtposss  49711  initocmd  50504  termolmd  50505