Theorem dmeqd 4931

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4723

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087  df-dm 4733

This theorem is referenced by:  rneq  4957  dmsnsnsng  5212  elxp4  5222  f10d  5615  fndmin  5750  1stvalg  6300  fo1st  6315  f1stres  6317  errn  6719  xpassen  7009  xpdom2  7010  frecuzrdgtclt  10673  s1dmg  11192  swrdval  11219  swrd0g  11231  shftdm  11373  ennnfonelemg  13014  ennnfonelem1  13018  ennnfonelemhdmp1  13020  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemex  13025  ennnfonelemhom  13026  isstruct2im  13082  isstruct2r  13083  setsvalg  13102  bassetsnn  13129  prdsval  13346  igsumvalx  13462  cnprcl2k  14920  psmetdmdm  15038  xmetdmdm  15070  blfvalps  15099  limccl  15373  ellimc3apf  15374  dvfvalap  15395  dvcj  15423  dvexp  15425  dvmptclx  15432  dvmptaddx  15433  dvmptmulx  15434  isuhgrm  15912  isushgrm  15913  uhgreq12g  15917  isuhgropm  15922  uhgrun  15927  isupgren  15936  upgrop  15945  isumgren  15946  upgr1edc  15962  upgrun  15965  umgrun  15967  isuspgren  15996  isusgren  15997  isuspgropen  16003  isusgropen  16004  ausgrusgrben  16007  usgrstrrepeen  16070  uspgr1edc  16079  vtxdgfval  16094  vtxdgop  16098  vtxdgfi0e  16101  vtxdeqd  16102  vtxdfifiun  16103  1loopgrvd2fi  16111  1loopgrvd0fi  16112  1hevtxdg0fi  16113  wksfval  16119  wlkres  16174  eupthsg  16240  eupthres  16252