Theorem dmeqi 5886

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

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

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-dm 5661

This theorem is used by:  dmxpin  5913  rncoss  5959  rncoeq  5963  rnun  6136  rninOLD  6138  rnxp  6162  rnxpss  6164  imainrect  6173  dmpropg  6215  dmtpop  6218  rnsnopg  6221  fntpg  6598  opabiotadm  6964  dffv2  6978  fvopab4ndm  7022  fnreseql  7045  dmoprab  7521  reldmmpo  7552  mpondm0  7659  elmpocl  7660  opabn1stprc  8067  bropopvvv  8099  bropfvvvv  8101  frrlem7  8303  frrlem14  8310  tfrlem8  8385  tfr1a  8395  tfr2a  8396  tfr2b  8397  rdgseg  8423  xpassen  9083  sbthlem5  9103  hartogslem1  9529  dmttrcl  9715  r1funlimOLD  9763  r1dmlim  9765  r1sucg  9769  r1limg  9771  rankf  9795  hsmexlem4  10500  axdc2lem  10519  dmaddpi  10968  dmmulpi  10969  dmaddsr  11163  dmmulsr  11164  axaddf  11223  axmulf  11224  divsfval  17712  mgmn0plusgf  18820  degenmgmopdm  19127  degenmgm2opdm  19131  mvdco  19652  symgsssg  19674  symgfisg  19675  pmtrdifellem2  19684  psgnunilem5  19701  matunitlindf  22989  ismbl  25840  volres  25842  efcvx  26769  dvrelog  26958  dvlog  26972  nosupcbv  28052  noinfcbv  28067  noetasuplem4  28086  noetainflem4  28090  dmcuts  28170  structiedg0val  29593  snstriedgval  29609  isuhgr  29631  isushgr  29632  isupgr  29655  isumgr  29666  isuspgr  29726  isusgr  29727  ushgredgedg  29803  ushgredgedgloop  29805  lfuhgr1v0e  29828  issubgr  29845  subgruhgredgd  29858  subumgredg2  29859  vtxdgfval  30041  vtxdlfgrval  30059  vtxdginducedm1lem2  30114  vtxdginducedm1fi  30118  finsumvtxdg2ssteplem4  30122  finsumvtxdg2size  30124  wlk2v2elem1  30749  dfhnorm2  31717  hlimcaui  31831  hhshsslem1  31862  dmadjss  32482  adjeu  32484  adj1o  32489  gsummpt2co  33602  cycpmrn  33697  tocyccntz  33698  extdgfialglem1  34317  prsdm  34539  mbfmcst  34884  eulerpartlemt  34996  0rrv  35076  coinflipspace  35106  bnj96  35488  bnj1398  35657  bnj1416  35662  bnj1450  35673  bnj1498  35684  bnj1501  35690  fineqvnttrclse  35775  fmla  36125  fmla0  36126  gonan0  36136  satffunlem2lem2  36150  fixun  36651  linedegen  36888  ssbnd  38702  ismgmOLD  38764  exidreslem  38791  n0el2  39247  dmxrn  39299  dmxrncnvepres  39344  dfsucmap2  39376  dmcoss3  39455  dmcoels  39459  dmmzp  43723  cnvrcl0  44610  dvsid  45300  dvsef  45301  modelaxreplem2  45947  dvsinax  46892  fperdvper  46898  dvcosax  46905  stoweidlem27  47006  fourierdlem57  47142  fourierdlem58  47143  fourierdlem62  47147  fourierdlem80  47165  fourierdlem94  47179  fourierdlem97  47182  fourierdlem113  47198  fouriersw  47210  fouriercn  47211  subsaliuncllem  47336  0ome  47508  hoi2toco  47586  isgrim  48949  usgrexmpl1lem  49088  usgrexmpl2lem  49093  gpgprismgr4cycllem8  49169  elbigofrcl  49631  dmtposss  49953  initocmd  50746  termolmd  50747