Theorem dmeqi 4923

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

Syntax hints:   = wceq 1395  dom cdm 4718

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 4083  df-dm 4728

This theorem is referenced by:  dmxpm  4943  dmxpid  4944  dmxpin  4945  rncoss  4994  rncoeq  4997  rnun  5136  rnin  5137  rnxpm  5157  rnxpss  5159  imainrect  5173  dmpropg  5200  dmtpop  5203  rnsnopg  5206  fntpg  5376  fnreseql  5744  dmoprab  6084  reldmmpo  6115  elmpocl  6199  tfrlem8  6462  tfr2a  6465  tfrlemi14d  6477  tfr1onlemres  6493  tfri1dALT  6495  tfrcllemres  6506  xpassen  6985  sbthlemi5  7124  casedm  7249  djudm  7268  ctssdccl  7274  dmaddpi  7508  dmmulpi  7509  dmaddpq  7562  dmmulpq  7563  axaddf  8051  axmulf  8052  ennnfonelemom  12974  ennnfonelemdm  12986  structiedg0val  15835  isuhgrm  15865  isushgrm  15866  isupgren  15889  isumgren  15899  isuspgren  15949  isusgren  15950  ushgredgedg  16018  ushgredgedgloop  16020