Theorem dmeqd 4978

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 4976	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   = wceq 1402  dom cdm 4769

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3711  df-pr 3712  df-op 3714  df-br 4126  df-dm 4779

This theorem is referenced by:  rneq  5004  dmsnsnsng  5260  elxp4  5270  f10d  5670  fndmin  5807  1stvalg  6366  fo1st  6381  f1stres  6383  errn  6819  xpassen  7118  xpdom2  7119  frecuzrdgtclt  10836  s1dmg  11371  swrdval  11398  swrd0g  11410  shftdm  11565  ennnfonelemg  13272  ennnfonelem1  13276  ennnfonelemhdmp1  13278  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemex  13283  ennnfonelemhom  13284  isstruct2im  13340  isstruct2r  13341  setsvalg  13360  bassetsnn  13387  gzsumvalx  13686  prdsval  14150  cnprcl2k  15230  psmetdmdm  15348  xmetdmdm  15380  blfvalps  15409  limccl  15683  ellimc3apf  15684  dvfvalap  15705  dvcj  15733  dvexp  15735  dvmptclx  15742  dvmptaddx  15743  dvmptmulx  15744  isuhgrm  16226  isushgrm  16227  uhgreq12g  16231  isuhgropm  16236  uhgrun  16241  isupgren  16250  upgrop  16259  isumgren  16260  upgr1edc  16276  umgr1een  16280  upgrun  16281  umgrun  16283  isuspgren  16312  isusgren  16313  isuspgropen  16319  isusgropen  16320  ausgrusgrben  16323  usgrstrrepeen  16386  uspgr1edc  16395  issubgr  16412  uhgrspansubgrlem  16431  vtxdgfval  16443  vtxdgop  16447  vtxdgfi0e  16450  vtxdeqd  16451  vtxdfifiun  16452  1loopgrvd2fi  16460  1loopgrvd0fi  16461  1hevtxdg0fi  16462  1hevtxdg1en  16463  1hegrvtxdg1fi  16464  p1evtxdeqfilem  16466  wksfval  16477  wlkres  16534  eupthsg  16600  eupthres  16612  trlsegvdeglem4  16618  trlsegvdeglem5  16619