Theorem coeq1d 5829

Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)

Hypothesis

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

Assertion

Ref	Expression
coeq1d	⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Proof of Theorem coeq1d

Step	Hyp	Ref	Expression
1		coeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		coeq1 5825	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Syntax hints:   → wi 4   = wceq 1559   ∘ ccom 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3919  df-br 5098  df-opab 5160  df-co 5652

This theorem is referenced by:  coeq12d  5832  fcof1oinvd  7272  domss2  9102  mapen  9107  mapfien  9348  hashfacen  14461  relexpsucnnr  15032  relexpsucnnl  15037  relexpsucr  15039  relexpsucrd  15040  relexpaddnn  15058  imasval  17532  cofuass  17913  cofulid  17914  setcinv  18114  catcisolem  18134  catciso  18135  yonedalem3b  18302  gsumvalx  18701  frmdup3lem  18891  symggrplem  18909  f1omvdco2  19479  symggen  19501  psgnunilem1  19524  gsumval3  19938  gsumzf1o  19943  znval  21575  znle2  21593  psrass1lem  21973  coe1add  22315  evls1fval  22370  evl1sca  22385  evl1var  22387  evls1var  22389  pf1mpf  22403  pf1ind  22406  tcphds  25281  dvnfval  25972  hocsubdir  31945  fcoinver  32764  fcobij  32883  cocnvf1o  32892  ccatws1f1olast  33091  symgfcoeu  33223  symgcom  33224  pmtrcnel2  33231  tocyc01  33259  cycpm2tr  33260  cycpmconjv  33283  cycpmconjslem1  33295  cycpmconjslem2  33296  cycpmconjs  33297  cyc3conja  33298  1arithidomlem2  33693  mplvrpmga  33803  mplvrpmrhm  33805  reprpmtf1o  34881  hgt750lemg  34909  subfacp1lem5  35495  mrsubffval  35818  mrsubfval  35819  mrsubrn  35824  elmrsubrn  35831  upixp  38189  ltrncoidN  40713  trlcoat  41308  trlcone  41313  cdlemg47a  41319  cdlemg47  41321  ltrnco4  41324  tendovalco  41350  tendoplcbv  41360  tendopl  41361  tendoplass  41368  tendo0pl  41376  tendoipl  41382  cdlemk45  41532  cdlemk53b  41541  cdlemk55a  41544  erngdvlem3  41575  erngdvlem3-rN  41583  tendocnv  41606  dvhvaddcbv  41674  dvhvaddval  41675  dvhvaddass  41682  dicvscacl  41776  cdlemn8  41789  dihordlem7b  41800  dihopelvalcpre  41833  aks6d1c6lem5  42755  relexp2  44214  relexpxpnnidm  44240  relexpiidm  44241  relexpmulnn  44246  relexpaddss  44255  trclfvcom  44260  trclfvdecomr  44265  frege131d  44301  dssmap2d  44559  fundcmpsurbijinjpreimafv  47974  gricushgr  48500  prcof21a  49973