Theorem dmeqi 4625

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

Syntax hints:   = wceq 1289   dom cdm 4428

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-un 3001  df-in 3003  df-ss 3010  df-sn 3447  df-pr 3448  df-op 3450  df-br 3838  df-dm 4438

This theorem is referenced by:  dmxpm  4644  dmxpinm  4645  rncoss  4691  rncoeq  4694  rnun  4827  rnin  4828  rnxpm  4847  rnxpss  4849  imainrect  4863  dmpropg  4890  dmtpop  4893  rnsnopg  4896  fntpg  5056  fnreseql  5393  dmoprab  5711  reldmmpt2  5738  elmpt2cl  5824  tfrlem8  6065  tfr2a  6068  tfrlemi14d  6080  tfr1onlemres  6096  tfri1dALT  6098  tfrcllemres  6109  xpassen  6526  sbthlemi5  6649  casedm  6756  djudm  6764  dmaddpi  6863  dmmulpi  6864  dmaddpq  6917  dmmulpq  6918