Theorem dmeqi 4959

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 4958	. 2 |- ( A = B -> dom A = dom B )
3	1, 2	ax-mp 5	1 |- dom A = dom B

Syntax hints:   = wceq 1398   dom cdm 4751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-sn 3697  df-pr 3698  df-op 3700  df-br 4112  df-dm 4761

This theorem is referenced by:  dmxpm  4979  dmxpid  4980  dmxpin  4981  rncoss  5030  rncoeq  5033  rnun  5173  rnin  5174  rnxpm  5194  rnxpss  5196  imainrect  5210  dmpropg  5237  dmtpop  5240  rnsnopg  5243  fntpg  5414  fnreseql  5790  dmoprab  6136  reldmmpo  6167  elmpocl  6251  opabn1stprc  6391  elmpom  6436  tfrlem8  6551  tfr2a  6554  tfrlemi14d  6566  tfr1onlemres  6582  tfri1dALT  6584  tfrcllemres  6595  xpassen  7083  sbthlemi5  7233  casedm  7379  djudm  7398  ctssdccl  7404  dmaddpi  7642  dmmulpi  7643  dmaddpq  7696  dmmulpq  7697  axaddf  8185  axmulf  8186  ennnfonelemom  13176  ennnfonelemdm  13188  structiedg0val  16052  isuhgrm  16083  isushgrm  16084  isupgren  16107  isumgren  16117  isuspgren  16169  isusgren  16170  ushgredgedg  16238  ushgredgedgloop  16240  issubgr  16269  subgruhgredgdm  16282  subumgredg2en  16283  vtxdgfval  16300