Theorem dmeqd 4963

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

Hypothesis

Ref	Expression
dmeqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
dmeqd	⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Proof of Theorem dmeqd

Step	Hyp	Ref	Expression
1		dmeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dmeq 4961	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4754

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115  df-dm 4764

This theorem is referenced by:  rneq  4989  dmsnsnsng  5245  elxp4  5255  f10d  5655  fndmin  5790  1stvalg  6349  fo1st  6364  f1stres  6366  errn  6802  xpassen  7094  xpdom2  7095  frecuzrdgtclt  10807  s1dmg  11338  swrdval  11365  swrd0g  11377  shftdm  11532  ennnfonelemg  13238  ennnfonelem1  13242  ennnfonelemhdmp1  13244  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemhom  13250  isstruct2im  13306  isstruct2r  13307  setsvalg  13326  bassetsnn  13353  igsumvalx  13652  prdsval  14115  cnprcl2k  15197  psmetdmdm  15315  xmetdmdm  15347  blfvalps  15376  limccl  15650  ellimc3apf  15651  dvfvalap  15672  dvcj  15700  dvexp  15702  dvmptclx  15709  dvmptaddx  15710  dvmptmulx  15711  isuhgrm  16192  isushgrm  16193  uhgreq12g  16197  isuhgropm  16202  uhgrun  16207  isupgren  16216  upgrop  16225  isumgren  16226  upgr1edc  16242  umgr1een  16246  upgrun  16247  umgrun  16249  isuspgren  16278  isusgren  16279  isuspgropen  16285  isusgropen  16286  ausgrusgrben  16289  usgrstrrepeen  16352  uspgr1edc  16361  issubgr  16378  uhgrspansubgrlem  16397  vtxdgfval  16409  vtxdgop  16413  vtxdgfi0e  16416  vtxdeqd  16417  vtxdfifiun  16418  1loopgrvd2fi  16426  1loopgrvd0fi  16427  1hevtxdg0fi  16428  1hevtxdg1en  16429  1hegrvtxdg1fi  16430  p1evtxdeqfilem  16432  wksfval  16443  wlkres  16500  eupthsg  16566  eupthres  16578  trlsegvdeglem4  16584  trlsegvdeglem5  16585