Theorem coeq1d 5804

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

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

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 3920  df-br 5093  df-opab 5155  df-co 5628

This theorem is referenced by:  coeq12d  5807  fcof1oinvd  7230  domss2  9053  mapen  9058  mapfien  9298  hashfacen  14361  relexpsucnnr  14932  relexpsucnnl  14937  relexpsucr  14939  relexpsucrd  14940  relexpaddnn  14958  imasval  17415  cofuass  17796  cofulid  17797  setcinv  17997  catcisolem  18017  catciso  18018  yonedalem3b  18185  gsumvalx  18550  frmdup3lem  18740  symggrplem  18758  f1omvdco2  19327  symggen  19349  psgnunilem1  19372  gsumval3  19786  gsumzf1o  19791  znval  21442  znle2  21460  psrass1lem  21839  coe1add  22148  evls1fval  22204  evl1sca  22219  evl1var  22221  evls1var  22223  pf1mpf  22237  pf1ind  22240  tcphds  25129  dvnfval  25822  hocsubdir  31733  fcoinver  32553  fcobij  32672  cocnvf1o  32681  ccatws1f1olast  32903  symgfcoeu  33033  symgcom  33034  pmtrcnel2  33041  tocyc01  33069  cycpm2tr  33070  cycpmconjv  33093  cycpmconjslem1  33105  cycpmconjslem2  33106  cycpmconjs  33107  cyc3conja  33108  1arithidomlem2  33482  mplvrpmga  33556  mplvrpmrhm  33558  reprpmtf1o  34610  hgt750lemg  34638  subfacp1lem5  35177  mrsubffval  35500  mrsubfval  35501  mrsubrn  35506  elmrsubrn  35513  upixp  37729  ltrncoidN  40127  trlcoat  40722  trlcone  40727  cdlemg47a  40733  cdlemg47  40735  ltrnco4  40738  tendovalco  40764  tendoplcbv  40774  tendopl  40775  tendoplass  40782  tendo0pl  40790  tendoipl  40796  cdlemk45  40946  cdlemk53b  40955  cdlemk55a  40958  erngdvlem3  40989  erngdvlem3-rN  40997  tendocnv  41020  dvhvaddcbv  41088  dvhvaddval  41089  dvhvaddass  41096  dicvscacl  41190  cdlemn8  41203  dihordlem7b  41214  dihopelvalcpre  41247  aks6d1c6lem5  42170  relexp2  43670  relexpxpnnidm  43696  relexpiidm  43697  relexpmulnn  43702  relexpaddss  43711  trclfvcom  43716  trclfvdecomr  43721  frege131d  43757  dssmap2d  44015  fundcmpsurbijinjpreimafv  47411  gricushgr  47921  prcof21a  49396