Theorem dmeqi 5325

Description: Equality inference for domain. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
dmeqi.1	|- A = B

Assertion

Ref	Expression
dmeqi	|- dom A = dom B

Proof of Theorem dmeqi

Step	Hyp	Ref	Expression
1		dmeqi.1	. 2 |- A = B
2		dmeq 5324	. 2 |- ( A = B -> dom A = dom B )
3	1, 2	ax-mp 5	1 |- dom A = dom B

Syntax hints:   = wceq 1483   dom cdm 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-dm 5124

This theorem is referenced by:  dmxp  5344  dmxpin  5346  rncoss  5386  rncoeq  5389  rnun  5541  rnin  5542  rnxp  5564  rnxpss  5566  imainrect  5575  dmpropg  5608  dmtpop  5611  rnsnopg  5614  fntpg  5948  opabiotadm  6260  dffv2  6271  fvopab4ndm  6307  fnreseql  6327  dmoprab  6741  reldmmpt2  6771  mpt2ndm0  6875  elmpt2cl  6876  opabn1stprc  7228  bropopvvv  7255  bropfvvvv  7257  wfrdmss  7421  wfrdmcl  7423  wfrlem16  7430  tfrlem8  7480  tfr1a  7490  tfr2a  7491  tfr2b  7492  rdgseg  7518  xpassen  8054  sbthlem5  8074  hartogslem1  8447  r1funlim  8629  r1sucg  8632  r1limg  8634  rankf  8657  hsmexlem4  9251  axdc2lem  9270  dmaddpi  9712  dmmulpi  9713  dmaddsr  9906  dmmulsr  9907  axaddf  9966  axmulf  9967  strlemor1OLD  15969  divsfval  16207  xpsfrnel2  16225  mvdco  17865  symgsssg  17887  symgfisg  17888  pmtrdifellem2  17897  psgnunilem5  17914  ismbl  23294  volres  23296  efcvx  24203  dvrelog  24383  dvlog  24397  structiedg0val  25911  snstriedgval  25930  isuhgr  25955  isushgr  25956  isupgr  25979  isumgr  25990  isuspgr  26047  isusgr  26048  ushgredgedg  26121  ushgredgedgloop  26123  lfuhgr1v0e  26146  issubgr  26163  subgruhgredgd  26176  subumgredg2  26177  vtxdgfval  26363  vtxdlfgrval  26381  vtxdginducedm1lem2  26436  vtxdginducedm1fi  26440  finsumvtxdg2ssteplem4  26444  finsumvtxdg2size  26446  wlk2v2elem1  27015  wlk2v2elem2  27016  dfhnorm2  27979  hlimcaui  28093  hhshsslem1  28124  dmadjss  28746  adjeu  28748  adj1o  28753  gsummpt2co  29780  prsdm  29960  mbfmcst  30321  eulerpartlemt  30433  0rrv  30513  coinflipspace  30542  bnj96  30935  bnj1398  31102  bnj1416  31107  bnj1450  31118  bnj1498  31129  bnj1501  31135  frrlem7  31790  noetalem3  31865  noetalem4  31866  dmscut  31918  fixun  32016  linedegen  32250  matunitlindf  33407  ssbnd  33587  ismgmOLD  33649  exidreslem  33676  n0el2  34103  dmmzp  37296  cnvrcl0  37932  dvsid  38530  dvsef  38531  dvsinax  40127  fperdvper  40133  dvcosax  40141  stoweidlem27  40244  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fourierdlem80  40403  fourierdlem94  40417  fourierdlem97  40420  fourierdlem113  40436  fouriersw  40448  fouriercn  40449  subsaliuncllem  40575  0ome  40743  hoi2toco  40821  elbigofrcl  42344