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  s1dmg  11077  shftdm  11104  ennnfonelemg  12745  ennnfonelem1  12749  ennnfonelemhdmp1  12751  ennnfonelemkh  12754  ennnfonelemhf1o  12755  ennnfonelemex  12756  ennnfonelemhom  12757  isstruct2im  12813  isstruct2r  12814  setsvalg  12833  prdsval  13076  igsumvalx  13192  cnprcl2k  14649  psmetdmdm  14767  xmetdmdm  14799  blfvalps  14828  limccl  15102  ellimc3apf  15103  dvfvalap  15124  dvcj  15152  dvexp  15154  dvmptclx  15161  dvmptaddx  15162  dvmptmulx  15163