Theorem dmeqd 4879

Description: Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
dmeqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
dmeqd	⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Proof of Theorem dmeqd

Step	Hyp	Ref	Expression
1		dmeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dmeq 4877	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   = wceq 1372  dom cdm 4674

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 4684

This theorem is referenced by:  rneq  4904  dmsnsnsng  5159  elxp4  5169  fndmin  5686  1stvalg  6227  fo1st  6242  f1stres  6244  errn  6641  xpassen  6924  xpdom2  6925  frecuzrdgtclt  10564  shftdm  11075  ennnfonelemg  12716  ennnfonelem1  12720  ennnfonelemhdmp1  12722  ennnfonelemkh  12725  ennnfonelemhf1o  12726  ennnfonelemex  12727  ennnfonelemhom  12728  isstruct2im  12784  isstruct2r  12785  setsvalg  12804  prdsval  13047  igsumvalx  13163  cnprcl2k  14620  psmetdmdm  14738  xmetdmdm  14770  blfvalps  14799  limccl  15073  ellimc3apf  15074  dvfvalap  15095  dvcj  15123  dvexp  15125  dvmptclx  15132  dvmptaddx  15133  dvmptmulx  15134