Theorem coeq1d 5825

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 5821	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∘ 𝐶) = (𝐵 ∘ 𝐶))

Syntax hints:   → wi 4   = wceq 1540   ∘ ccom 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-br 5108  df-opab 5170  df-co 5647

This theorem is referenced by:  coeq12d  5828  fcof1oinvd  7268  domss2  9100  mapen  9105  mapfien  9359  hashfacen  14419  relexpsucnnr  14991  relexpsucnnl  14996  relexpsucr  14998  relexpsucrd  14999  relexpaddnn  15017  imasval  17474  cofuass  17851  cofulid  17852  setcinv  18052  catcisolem  18072  catciso  18073  yonedalem3b  18240  gsumvalx  18603  frmdup3lem  18793  symggrplem  18811  f1omvdco2  19378  symggen  19400  psgnunilem1  19423  gsumval3  19837  gsumzf1o  19842  znval  21445  znle2  21463  psrass1lem  21841  coe1add  22150  evls1fval  22206  evl1sca  22221  evl1var  22223  evls1var  22225  pf1mpf  22239  pf1ind  22242  tcphds  25131  dvnfval  25824  hocsubdir  31714  fcoinver  32533  fcobij  32645  ccatws1f1olast  32874  symgfcoeu  33039  symgcom  33040  pmtrcnel2  33047  tocyc01  33075  cycpm2tr  33076  cycpmconjv  33099  cycpmconjslem1  33111  cycpmconjslem2  33112  cycpmconjs  33113  cyc3conja  33114  1arithidomlem2  33507  reprpmtf1o  34617  hgt750lemg  34645  subfacp1lem5  35171  mrsubffval  35494  mrsubfval  35495  mrsubrn  35500  elmrsubrn  35507  upixp  37723  ltrncoidN  40122  trlcoat  40717  trlcone  40722  cdlemg47a  40728  cdlemg47  40730  ltrnco4  40733  tendovalco  40759  tendoplcbv  40769  tendopl  40770  tendoplass  40777  tendo0pl  40785  tendoipl  40791  cdlemk45  40941  cdlemk53b  40950  cdlemk55a  40953  erngdvlem3  40984  erngdvlem3-rN  40992  tendocnv  41015  dvhvaddcbv  41083  dvhvaddval  41084  dvhvaddass  41091  dicvscacl  41185  cdlemn8  41198  dihordlem7b  41209  dihopelvalcpre  41242  aks6d1c6lem5  42165  relexp2  43666  relexpxpnnidm  43692  relexpiidm  43693  relexpmulnn  43698  relexpaddss  43707  trclfvcom  43712  trclfvdecomr  43717  frege131d  43753  dssmap2d  44011  fundcmpsurbijinjpreimafv  47408  gricushgr  47917  prcof21a  49380