Theorem dmeqi 5768

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

Syntax hints:   = wceq 1533  dom cdm 5550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-br 5060  df-dm 5560

This theorem is referenced by:  dmxp  5794  dmxpin  5796  rncoss  5838  rncoeq  5841  rnun  5999  rnin  6000  rnxp  6022  rnxpss  6024  imainrect  6033  dmpropg  6067  dmtpop  6070  rnsnopg  6073  fntpg  6409  opabiotadm  6740  dffv2  6751  fvopab4ndm  6792  fnreseql  6813  dmoprab  7249  reldmmpo  7279  mpondm0  7380  elmpocl  7381  opabn1stprc  7750  bropopvvv  7779  bropfvvvv  7781  wfrdmss  7955  wfrdmcl  7957  wfrlem16  7964  tfrlem8  8014  tfr1a  8024  tfr2a  8025  tfr2b  8026  rdgseg  8052  xpassen  8605  sbthlem5  8625  hartogslem1  9000  r1funlim  9189  r1sucg  9192  r1limg  9194  rankf  9217  hsmexlem4  9845  axdc2lem  9864  dmaddpi  10306  dmmulpi  10307  dmaddsr  10501  dmmulsr  10502  axaddf  10561  axmulf  10562  divsfval  16814  mvdco  18567  symgsssg  18589  symgfisg  18590  pmtrdifellem2  18599  psgnunilem5  18616  ismbl  24121  volres  24123  efcvx  25031  dvrelog  25214  dvlog  25228  structiedg0val  26801  snstriedgval  26817  isuhgr  26839  isushgr  26840  isupgr  26863  isumgr  26874  isuspgr  26931  isusgr  26932  ushgredgedg  27005  ushgredgedgloop  27007  lfuhgr1v0e  27030  issubgr  27047  subgruhgredgd  27060  subumgredg2  27061  vtxdgfval  27243  vtxdlfgrval  27261  vtxdginducedm1lem2  27316  vtxdginducedm1fi  27320  finsumvtxdg2ssteplem4  27324  finsumvtxdg2size  27326  wlk2v2elem1  27928  dfhnorm2  28893  hlimcaui  29007  hhshsslem1  29038  dmadjss  29658  adjeu  29660  adj1o  29665  gsummpt2co  30681  cycpmrn  30780  tocyccntz  30781  prsdm  31152  mbfmcst  31512  eulerpartlemt  31624  0rrv  31704  coinflipspace  31733  bnj96  32132  bnj1398  32301  bnj1416  32306  bnj1450  32317  bnj1498  32328  bnj1501  32334  fmla  32623  fmla0  32624  gonan0  32634  satffunlem2lem2  32648  frrlem7  33124  frrlem14  33131  noetalem3  33214  noetalem4  33215  dmscut  33267  fixun  33365  linedegen  33599  matunitlindf  34884  ssbnd  35060  ismgmOLD  35122  exidreslem  35149  n0el2  35584  dmcoss3  35687  dmcoels  35691  dmmzp  39323  cnvrcl0  39978  dvsid  40656  dvsef  40657  dvsinax  42189  fperdvper  42195  dvcosax  42203  stoweidlem27  42305  fourierdlem57  42441  fourierdlem58  42442  fourierdlem62  42446  fourierdlem80  42464  fourierdlem94  42478  fourierdlem97  42481  fourierdlem113  42497  fouriersw  42509  fouriercn  42510  subsaliuncllem  42633  0ome  42804  hoi2toco  42882  elbigofrcl  44603