Theorem dmeqd 4939

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

Syntax hints:   -> wi 4   = wceq 1398   dom cdm 4731

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094  df-dm 4741

This theorem is referenced by:  rneq  4965  dmsnsnsng  5221  elxp4  5231  f10d  5628  fndmin  5763  1stvalg  6314  fo1st  6329  f1stres  6331  errn  6767  xpassen  7057  xpdom2  7058  frecuzrdgtclt  10727  s1dmg  11249  swrdval  11276  swrd0g  11288  shftdm  11443  ennnfonelemg  13085  ennnfonelem1  13089  ennnfonelemhdmp1  13091  ennnfonelemkh  13094  ennnfonelemhf1o  13095  ennnfonelemex  13096  ennnfonelemhom  13097  isstruct2im  13153  isstruct2r  13154  setsvalg  13173  bassetsnn  13200  prdsval  13417  igsumvalx  13533  cnprcl2k  14997  psmetdmdm  15115  xmetdmdm  15147  blfvalps  15176  limccl  15450  ellimc3apf  15451  dvfvalap  15472  dvcj  15500  dvexp  15502  dvmptclx  15509  dvmptaddx  15510  dvmptmulx  15511  isuhgrm  15992  isushgrm  15993  uhgreq12g  15997  isuhgropm  16002  uhgrun  16007  isupgren  16016  upgrop  16025  isumgren  16026  upgr1edc  16042  umgr1een  16046  upgrun  16047  umgrun  16049  isuspgren  16078  isusgren  16079  isuspgropen  16085  isusgropen  16086  ausgrusgrben  16089  usgrstrrepeen  16152  uspgr1edc  16161  issubgr  16178  uhgrspansubgrlem  16197  vtxdgfval  16209  vtxdgop  16213  vtxdgfi0e  16216  vtxdeqd  16217  vtxdfifiun  16218  1loopgrvd2fi  16226  1loopgrvd0fi  16227  1hevtxdg0fi  16228  1hevtxdg1en  16229  1hegrvtxdg1fi  16230  p1evtxdeqfilem  16232  wksfval  16243  wlkres  16300  eupthsg  16366  eupthres  16378  trlsegvdeglem4  16384  trlsegvdeglem5  16385