Theorem dmeqd 4925

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

Hypothesis

Ref	Expression
dmeqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
dmeqd	|- ( ph -> dom A = dom B )

Proof of Theorem dmeqd

Step	Hyp	Ref	Expression
1		dmeqd.1	. 2 |- ( ph -> A = B )
2		dmeq 4923	. 2 |- ( A = B -> dom A = dom B )
3	1, 2	syl 14	1 |- ( ph -> dom A = dom B )

Syntax hints:   -> wi 4   = wceq 1395   dom cdm 4719

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 4084  df-dm 4729

This theorem is referenced by:  rneq  4951  dmsnsnsng  5206  elxp4  5216  f10d  5607  fndmin  5742  1stvalg  6288  fo1st  6303  f1stres  6305  errn  6702  xpassen  6989  xpdom2  6990  frecuzrdgtclt  10643  s1dmg  11158  swrdval  11180  swrd0g  11192  shftdm  11333  ennnfonelemg  12974  ennnfonelem1  12978  ennnfonelemhdmp1  12980  ennnfonelemkh  12983  ennnfonelemhf1o  12984  ennnfonelemex  12985  ennnfonelemhom  12986  isstruct2im  13042  isstruct2r  13043  setsvalg  13062  bassetsnn  13089  prdsval  13306  igsumvalx  13422  cnprcl2k  14880  psmetdmdm  14998  xmetdmdm  15030  blfvalps  15059  limccl  15333  ellimc3apf  15334  dvfvalap  15355  dvcj  15383  dvexp  15385  dvmptclx  15392  dvmptaddx  15393  dvmptmulx  15394  isuhgrm  15871  isushgrm  15872  uhgreq12g  15876  isuhgropm  15881  uhgrun  15886  isupgren  15895  upgrop  15904  isumgren  15905  upgr1edc  15921  upgrun  15924  umgrun  15926  isuspgren  15955  isusgren  15956  isuspgropen  15962  isusgropen  15963  ausgrusgrben  15966  usgrstrrepeen  16029  wksfval  16035