Theorem dmeqi 4931

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

Syntax hints:   = wceq 1397  dom cdm 4724

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-un 3203  df-in 3205  df-ss 3212  df-sn 3674  df-pr 3675  df-op 3677  df-br 4088  df-dm 4734

This theorem is referenced by:  dmxpm  4951  dmxpid  4952  dmxpin  4953  rncoss  5002  rncoeq  5005  rnun  5144  rnin  5145  rnxpm  5165  rnxpss  5167  imainrect  5181  dmpropg  5208  dmtpop  5211  rnsnopg  5214  fntpg  5385  fnreseql  5757  dmoprab  6104  reldmmpo  6135  elmpocl  6219  opabn1stprc  6360  elmpom  6405  tfrlem8  6486  tfr2a  6489  tfrlemi14d  6501  tfr1onlemres  6517  tfri1dALT  6519  tfrcllemres  6530  xpassen  7016  sbthlemi5  7162  casedm  7287  djudm  7306  ctssdccl  7312  dmaddpi  7547  dmmulpi  7548  dmaddpq  7601  dmmulpq  7602  axaddf  8090  axmulf  8091  ennnfonelemom  13049  ennnfonelemdm  13061  structiedg0val  15917  isuhgrm  15948  isushgrm  15949  isupgren  15972  isumgren  15982  isuspgren  16034  isusgren  16035  ushgredgedg  16103  ushgredgedgloop  16105  issubgr  16134  subgruhgredgdm  16147  subumgredg2en  16148  vtxdgfval  16165