Theorem dmeqi 5853

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

Syntax hints:   = wceq 1542  dom cdm 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-dm 5634

This theorem is referenced by:  dmxpin  5880  rncoss  5926  rncoeq  5931  rnun  6103  rnin  6104  rnxp  6128  rnxpss  6130  imainrect  6139  dmpropg  6173  dmtpop  6176  rnsnopg  6179  fntpg  6552  opabiotadm  6915  dffv2  6929  fvopab4ndm  6972  fnreseql  6994  dmoprab  7463  reldmmpo  7494  mpondm0  7600  elmpocl  7601  opabn1stprc  8004  bropopvvv  8033  bropfvvvv  8035  frrlem7  8235  frrlem14  8242  tfrlem8  8316  tfr1a  8326  tfr2a  8327  tfr2b  8328  rdgseg  8354  xpassen  9002  sbthlem5  9022  hartogslem1  9450  dmttrcl  9633  r1funlim  9681  r1sucg  9684  r1limg  9686  rankf  9709  hsmexlem4  10342  axdc2lem  10361  dmaddpi  10804  dmmulpi  10805  dmaddsr  10999  dmmulsr  11000  axaddf  11059  axmulf  11060  divsfval  17502  mvdco  19411  symgsssg  19433  symgfisg  19434  pmtrdifellem2  19443  psgnunilem5  19460  ismbl  25503  volres  25505  efcvx  26427  dvrelog  26614  dvlog  26628  nosupcbv  27680  noinfcbv  27695  noetasuplem4  27714  noetainflem4  27718  dmcuts  27797  structiedg0val  29105  snstriedgval  29121  isuhgr  29143  isushgr  29144  isupgr  29167  isumgr  29178  isuspgr  29235  isusgr  29236  ushgredgedg  29312  ushgredgedgloop  29314  lfuhgr1v0e  29337  issubgr  29354  subgruhgredgd  29367  subumgredg2  29368  vtxdgfval  29551  vtxdlfgrval  29569  vtxdginducedm1lem2  29624  vtxdginducedm1fi  29628  finsumvtxdg2ssteplem4  29632  finsumvtxdg2size  29634  wlk2v2elem1  30240  dfhnorm2  31208  hlimcaui  31322  hhshsslem1  31353  dmadjss  31973  adjeu  31975  adj1o  31980  gsummpt2co  33124  cycpmrn  33219  tocyccntz  33220  extdgfialglem1  33852  prsdm  34074  mbfmcst  34419  eulerpartlemt  34531  0rrv  34611  coinflipspace  34641  bnj96  35023  bnj1398  35192  bnj1416  35197  bnj1450  35208  bnj1498  35219  bnj1501  35225  fineqvnttrclse  35284  fmla  35579  fmla0  35580  gonan0  35590  satffunlem2lem2  35604  fixun  36105  linedegen  36341  matunitlindf  37953  ssbnd  38123  ismgmOLD  38185  exidreslem  38212  n0el2  38670  dmxrn  38722  dmxrncnvepres  38767  dfsucmap2  38799  dmcoss3  38878  dmcoels  38882  dmmzp  43179  cnvrcl0  44070  dvsid  44776  dvsef  44777  modelaxreplem2  45424  dvsinax  46359  fperdvper  46365  dvcosax  46372  stoweidlem27  46473  fourierdlem57  46609  fourierdlem58  46610  fourierdlem62  46614  fourierdlem80  46632  fourierdlem94  46646  fourierdlem97  46649  fourierdlem113  46665  fouriersw  46677  fouriercn  46678  subsaliuncllem  46803  0ome  46975  hoi2toco  47053  isgrim  48370  usgrexmpl1lem  48509  usgrexmpl2lem  48514  gpgprismgr4cycllem8  48590  elbigofrcl  49038  dmtposss  49363  initocmd  50156  termolmd  50157