Theorem dmeqd 4925

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

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

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084  df-dm 4729

This theorem is referenced by:  rneq  4951  dmsnsnsng  5206  elxp4  5216  f10d  5609  fndmin  5744  1stvalg  6294  fo1st  6309  f1stres  6311  errn  6710  xpassen  6997  xpdom2  6998  frecuzrdgtclt  10655  s1dmg  11173  swrdval  11196  swrd0g  11208  shftdm  11349  ennnfonelemg  12990  ennnfonelem1  12994  ennnfonelemhdmp1  12996  ennnfonelemkh  12999  ennnfonelemhf1o  13000  ennnfonelemex  13001  ennnfonelemhom  13002  isstruct2im  13058  isstruct2r  13059  setsvalg  13078  bassetsnn  13105  prdsval  13322  igsumvalx  13438  cnprcl2k  14896  psmetdmdm  15014  xmetdmdm  15046  blfvalps  15075  limccl  15349  ellimc3apf  15350  dvfvalap  15371  dvcj  15399  dvexp  15401  dvmptclx  15408  dvmptaddx  15409  dvmptmulx  15410  isuhgrm  15887  isushgrm  15888  uhgreq12g  15892  isuhgropm  15897  uhgrun  15902  isupgren  15911  upgrop  15920  isumgren  15921  upgr1edc  15937  upgrun  15940  umgrun  15942  isuspgren  15971  isusgren  15972  isuspgropen  15978  isusgropen  15979  ausgrusgrben  15982  usgrstrrepeen  16045  vtxdgfval  16048  vtxdgop  16052  vtxdgfi0e  16055  vtxdeqd  16056  vtxdfifiun  16057  wksfval  16068  wlkres  16123