Theorem dmeqi 4924

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

Syntax hints:   = wceq 1395   dom cdm 4719

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084  df-dm 4729

This theorem is referenced by:  dmxpm  4944  dmxpid  4945  dmxpin  4946  rncoss  4995  rncoeq  4998  rnun  5137  rnin  5138  rnxpm  5158  rnxpss  5160  imainrect  5174  dmpropg  5201  dmtpop  5204  rnsnopg  5207  fntpg  5377  fnreseql  5745  dmoprab  6085  reldmmpo  6116  elmpocl  6200  tfrlem8  6464  tfr2a  6467  tfrlemi14d  6479  tfr1onlemres  6495  tfri1dALT  6497  tfrcllemres  6508  xpassen  6989  sbthlemi5  7128  casedm  7253  djudm  7272  ctssdccl  7278  dmaddpi  7512  dmmulpi  7513  dmaddpq  7566  dmmulpq  7567  axaddf  8055  axmulf  8056  ennnfonelemom  12979  ennnfonelemdm  12991  structiedg0val  15841  isuhgrm  15871  isushgrm  15872  isupgren  15895  isumgren  15905  isuspgren  15955  isusgren  15956  ushgredgedg  16024  ushgredgedgloop  16026