Theorem dmeqd 4830

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

Syntax hints:   -> wi 4   = wceq 1353   dom cdm 4627

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005  df-dm 4637

This theorem is referenced by:  rneq  4855  dmsnsnsng  5107  elxp4  5117  fndmin  5624  1stvalg  6143  fo1st  6158  f1stres  6160  errn  6557  xpassen  6830  xpdom2  6831  frecuzrdgtclt  10421  shftdm  10831  ennnfonelemg  12404  ennnfonelem1  12408  ennnfonelemhdmp1  12410  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemex  12415  ennnfonelemhom  12416  isstruct2im  12472  isstruct2r  12473  setsvalg  12492  cnprcl2k  13709  psmetdmdm  13827  xmetdmdm  13859  blfvalps  13888  limccl  14131  ellimc3apf  14132  dvfvalap  14153  dvcj  14176  dvexp  14178  dvmptclx  14183  dvmptaddx  14184  dvmptmulx  14185