Theorem dmeqd 4933

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

Syntax hints:   -> wi 4   = wceq 1397   dom cdm 4725

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089  df-dm 4735

This theorem is referenced by:  rneq  4959  dmsnsnsng  5214  elxp4  5224  f10d  5619  fndmin  5754  1stvalg  6305  fo1st  6320  f1stres  6322  errn  6724  xpassen  7014  xpdom2  7015  frecuzrdgtclt  10684  s1dmg  11206  swrdval  11233  swrd0g  11245  shftdm  11400  ennnfonelemg  13042  ennnfonelem1  13046  ennnfonelemhdmp1  13048  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemex  13053  ennnfonelemhom  13054  isstruct2im  13110  isstruct2r  13111  setsvalg  13130  bassetsnn  13157  prdsval  13374  igsumvalx  13490  cnprcl2k  14949  psmetdmdm  15067  xmetdmdm  15099  blfvalps  15128  limccl  15402  ellimc3apf  15403  dvfvalap  15424  dvcj  15452  dvexp  15454  dvmptclx  15461  dvmptaddx  15462  dvmptmulx  15463  isuhgrm  15941  isushgrm  15942  uhgreq12g  15946  isuhgropm  15951  uhgrun  15956  isupgren  15965  upgrop  15974  isumgren  15975  upgr1edc  15991  umgr1een  15995  upgrun  15996  umgrun  15998  isuspgren  16027  isusgren  16028  isuspgropen  16034  isusgropen  16035  ausgrusgrben  16038  usgrstrrepeen  16101  uspgr1edc  16110  issubgr  16127  uhgrspansubgrlem  16146  vtxdgfval  16158  vtxdgop  16162  vtxdgfi0e  16165  vtxdeqd  16166  vtxdfifiun  16167  1loopgrvd2fi  16175  1loopgrvd0fi  16176  1hevtxdg0fi  16177  1hevtxdg1en  16178  1hegrvtxdg1fi  16179  p1evtxdeqfilem  16181  wksfval  16192  wlkres  16249  eupthsg  16315  eupthres  16327  trlsegvdeglem4  16333  trlsegvdeglem5  16334