Theorem dmeqi 4877

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

Syntax hints:   = wceq 1372  dom cdm 4673

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 4683

This theorem is referenced by:  dmxpm  4896  dmxpid  4897  dmxpin  4898  rncoss  4946  rncoeq  4949  rnun  5088  rnin  5089  rnxpm  5109  rnxpss  5111  imainrect  5125  dmpropg  5152  dmtpop  5155  rnsnopg  5158  fntpg  5324  fnreseql  5684  dmoprab  6016  reldmmpo  6047  elmpocl  6131  tfrlem8  6394  tfr2a  6397  tfrlemi14d  6409  tfr1onlemres  6425  tfri1dALT  6427  tfrcllemres  6438  xpassen  6907  sbthlemi5  7045  casedm  7170  djudm  7189  ctssdccl  7195  dmaddpi  7420  dmmulpi  7421  dmaddpq  7474  dmmulpq  7475  axaddf  7963  axmulf  7964  ennnfonelemom  12698  ennnfonelemdm  12710