Theorem dmeqi 4878

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

Syntax hints:   = wceq 1372  dom cdm 4674

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044  df-dm 4684

This theorem is referenced by:  dmxpm  4897  dmxpid  4898  dmxpin  4899  rncoss  4948  rncoeq  4951  rnun  5090  rnin  5091  rnxpm  5111  rnxpss  5113  imainrect  5127  dmpropg  5154  dmtpop  5157  rnsnopg  5160  fntpg  5329  fnreseql  5689  dmoprab  6025  reldmmpo  6056  elmpocl  6140  tfrlem8  6403  tfr2a  6406  tfrlemi14d  6418  tfr1onlemres  6434  tfri1dALT  6436  tfrcllemres  6447  xpassen  6924  sbthlemi5  7062  casedm  7187  djudm  7206  ctssdccl  7212  dmaddpi  7437  dmmulpi  7438  dmaddpq  7491  dmmulpq  7492  axaddf  7980  axmulf  7981  ennnfonelemom  12721  ennnfonelemdm  12733  structiedg0val  15579