Theorem dmeqi 4863

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

Syntax hints:   = wceq 1364  dom cdm 4659

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-sn 3624  df-pr 3625  df-op 3627  df-br 4030  df-dm 4669

This theorem is referenced by:  dmxpm  4882  dmxpid  4883  dmxpin  4884  rncoss  4932  rncoeq  4935  rnun  5074  rnin  5075  rnxpm  5095  rnxpss  5097  imainrect  5111  dmpropg  5138  dmtpop  5141  rnsnopg  5144  fntpg  5310  fnreseql  5668  dmoprab  5999  reldmmpo  6030  elmpocl  6113  tfrlem8  6371  tfr2a  6374  tfrlemi14d  6386  tfr1onlemres  6402  tfri1dALT  6404  tfrcllemres  6415  xpassen  6884  sbthlemi5  7020  casedm  7145  djudm  7164  ctssdccl  7170  dmaddpi  7385  dmmulpi  7386  dmaddpq  7439  dmmulpq  7440  axaddf  7928  axmulf  7929  ennnfonelemom  12565  ennnfonelemdm  12577