Theorem dmeqd 4841

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 4839	. 2 |- ( A = B -> dom A = dom B )
3	1, 2	syl 14	1 |- ( ph -> dom A = dom B )

Syntax hints:   -> wi 4   = wceq 1363   dom cdm 4638

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-un 3145  df-in 3147  df-ss 3154  df-sn 3610  df-pr 3611  df-op 3613  df-br 4016  df-dm 4648

This theorem is referenced by:  rneq  4866  dmsnsnsng  5118  elxp4  5128  fndmin  5636  1stvalg  6157  fo1st  6172  f1stres  6174  errn  6571  xpassen  6844  xpdom2  6845  frecuzrdgtclt  10435  shftdm  10845  ennnfonelemg  12418  ennnfonelem1  12422  ennnfonelemhdmp1  12424  ennnfonelemkh  12427  ennnfonelemhf1o  12428  ennnfonelemex  12429  ennnfonelemhom  12430  isstruct2im  12486  isstruct2r  12487  setsvalg  12506  cnprcl2k  14002  psmetdmdm  14120  xmetdmdm  14152  blfvalps  14181  limccl  14424  ellimc3apf  14425  dvfvalap  14446  dvcj  14469  dvexp  14471  dvmptclx  14476  dvmptaddx  14477  dvmptmulx  14478