Theorem dmeqi 4888

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

Syntax hints:   = wceq 1373  dom cdm 4683

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3644  df-pr 3645  df-op 3647  df-br 4052  df-dm 4693

This theorem is referenced by:  dmxpm  4907  dmxpid  4908  dmxpin  4909  rncoss  4958  rncoeq  4961  rnun  5100  rnin  5101  rnxpm  5121  rnxpss  5123  imainrect  5137  dmpropg  5164  dmtpop  5167  rnsnopg  5170  fntpg  5339  fnreseql  5703  dmoprab  6039  reldmmpo  6070  elmpocl  6154  tfrlem8  6417  tfr2a  6420  tfrlemi14d  6432  tfr1onlemres  6448  tfri1dALT  6450  tfrcllemres  6461  xpassen  6940  sbthlemi5  7078  casedm  7203  djudm  7222  ctssdccl  7228  dmaddpi  7458  dmmulpi  7459  dmaddpq  7512  dmmulpq  7513  axaddf  8001  axmulf  8002  ennnfonelemom  12854  ennnfonelemdm  12866  structiedg0val  15714  isuhgrm  15742  isushgrm  15743  isupgren  15766  isumgren  15776