Theorem dmeqi 5773

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

Syntax hints:   = wceq 1537  dom cdm 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-dm 5565

This theorem is referenced by:  dmxp  5799  dmxpin  5801  rncoss  5843  rncoeq  5846  rnun  6004  rnin  6005  rnxp  6027  rnxpss  6029  imainrect  6038  dmpropg  6072  dmtpop  6075  rnsnopg  6078  fntpg  6414  opabiotadm  6745  dffv2  6756  fvopab4ndm  6797  fnreseql  6818  dmoprab  7255  reldmmpo  7285  mpondm0  7386  elmpocl  7387  opabn1stprc  7756  bropopvvv  7785  bropfvvvv  7787  wfrdmss  7961  wfrdmcl  7963  wfrlem16  7970  tfrlem8  8020  tfr1a  8030  tfr2a  8031  tfr2b  8032  rdgseg  8058  xpassen  8611  sbthlem5  8631  hartogslem1  9006  r1funlim  9195  r1sucg  9198  r1limg  9200  rankf  9223  hsmexlem4  9851  axdc2lem  9870  dmaddpi  10312  dmmulpi  10313  dmaddsr  10507  dmmulsr  10508  axaddf  10567  axmulf  10568  divsfval  16820  mvdco  18573  symgsssg  18595  symgfisg  18596  pmtrdifellem2  18605  psgnunilem5  18622  ismbl  24127  volres  24129  efcvx  25037  dvrelog  25220  dvlog  25234  structiedg0val  26807  snstriedgval  26823  isuhgr  26845  isushgr  26846  isupgr  26869  isumgr  26880  isuspgr  26937  isusgr  26938  ushgredgedg  27011  ushgredgedgloop  27013  lfuhgr1v0e  27036  issubgr  27053  subgruhgredgd  27066  subumgredg2  27067  vtxdgfval  27249  vtxdlfgrval  27267  vtxdginducedm1lem2  27322  vtxdginducedm1fi  27326  finsumvtxdg2ssteplem4  27330  finsumvtxdg2size  27332  wlk2v2elem1  27934  dfhnorm2  28899  hlimcaui  29013  hhshsslem1  29044  dmadjss  29664  adjeu  29666  adj1o  29671  gsummpt2co  30686  cycpmrn  30785  tocyccntz  30786  prsdm  31157  mbfmcst  31517  eulerpartlemt  31629  0rrv  31709  coinflipspace  31738  bnj96  32137  bnj1398  32306  bnj1416  32311  bnj1450  32322  bnj1498  32333  bnj1501  32339  fmla  32628  fmla0  32629  gonan0  32639  satffunlem2lem2  32653  frrlem7  33129  frrlem14  33136  noetalem3  33219  noetalem4  33220  dmscut  33272  fixun  33370  linedegen  33604  matunitlindf  34905  ssbnd  35081  ismgmOLD  35143  exidreslem  35170  n0el2  35605  dmcoss3  35708  dmcoels  35712  dmmzp  39379  cnvrcl0  40034  dvsid  40712  dvsef  40713  dvsinax  42246  fperdvper  42252  dvcosax  42260  stoweidlem27  42361  fourierdlem57  42497  fourierdlem58  42498  fourierdlem62  42502  fourierdlem80  42520  fourierdlem94  42534  fourierdlem97  42537  fourierdlem113  42553  fouriersw  42565  fouriercn  42566  subsaliuncllem  42689  0ome  42860  hoi2toco  42938  elbigofrcl  44659