Theorem dmeqd 4924

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 4922	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4718

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083  df-dm 4728

This theorem is referenced by:  rneq  4950  dmsnsnsng  5205  elxp4  5215  f10d  5606  fndmin  5741  1stvalg  6286  fo1st  6301  f1stres  6303  errn  6700  xpassen  6985  xpdom2  6986  frecuzrdgtclt  10638  s1dmg  11153  swrdval  11175  swrd0g  11187  shftdm  11328  ennnfonelemg  12969  ennnfonelem1  12973  ennnfonelemhdmp1  12975  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemex  12980  ennnfonelemhom  12981  isstruct2im  13037  isstruct2r  13038  setsvalg  13057  bassetsnn  13084  prdsval  13301  igsumvalx  13417  cnprcl2k  14874  psmetdmdm  14992  xmetdmdm  15024  blfvalps  15053  limccl  15327  ellimc3apf  15328  dvfvalap  15349  dvcj  15377  dvexp  15379  dvmptclx  15386  dvmptaddx  15387  dvmptmulx  15388  isuhgrm  15865  isushgrm  15866  uhgreq12g  15870  isuhgropm  15875  uhgrun  15880  isupgren  15889  upgrop  15898  isumgren  15899  upgr1edc  15915  upgrun  15918  umgrun  15920  isuspgren  15949  isusgren  15950  isuspgropen  15956  isusgropen  15957  ausgrusgrben  15960  usgrstrrepeen  16023  wksfval  16028