Theorem coeq1d 5810

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

Syntax hints:   → wi 4   = wceq 1541   ∘ ccom 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-br 5099  df-opab 5161  df-co 5633

This theorem is referenced by:  coeq12d  5813  fcof1oinvd  7239  domss2  9064  mapen  9069  mapfien  9311  hashfacen  14377  relexpsucnnr  14948  relexpsucnnl  14953  relexpsucr  14955  relexpsucrd  14956  relexpaddnn  14974  imasval  17432  cofuass  17813  cofulid  17814  setcinv  18014  catcisolem  18034  catciso  18035  yonedalem3b  18202  gsumvalx  18601  frmdup3lem  18791  symggrplem  18809  f1omvdco2  19377  symggen  19399  psgnunilem1  19422  gsumval3  19836  gsumzf1o  19841  znval  21490  znle2  21508  psrass1lem  21888  coe1add  22206  evls1fval  22263  evl1sca  22278  evl1var  22280  evls1var  22282  pf1mpf  22296  pf1ind  22299  tcphds  25187  dvnfval  25880  hocsubdir  31860  fcoinver  32679  fcobij  32799  cocnvf1o  32808  ccatws1f1olast  33034  symgfcoeu  33164  symgcom  33165  pmtrcnel2  33172  tocyc01  33200  cycpm2tr  33201  cycpmconjv  33224  cycpmconjslem1  33236  cycpmconjslem2  33237  cycpmconjs  33238  cyc3conja  33239  1arithidomlem2  33617  mplvrpmga  33710  mplvrpmrhm  33712  reprpmtf1o  34783  hgt750lemg  34811  subfacp1lem5  35378  mrsubffval  35701  mrsubfval  35702  mrsubrn  35707  elmrsubrn  35714  upixp  37930  ltrncoidN  40388  trlcoat  40983  trlcone  40988  cdlemg47a  40994  cdlemg47  40996  ltrnco4  40999  tendovalco  41025  tendoplcbv  41035  tendopl  41036  tendoplass  41043  tendo0pl  41051  tendoipl  41057  cdlemk45  41207  cdlemk53b  41216  cdlemk55a  41219  erngdvlem3  41250  erngdvlem3-rN  41258  tendocnv  41281  dvhvaddcbv  41349  dvhvaddval  41350  dvhvaddass  41357  dicvscacl  41451  cdlemn8  41464  dihordlem7b  41475  dihopelvalcpre  41508  aks6d1c6lem5  42431  relexp2  43918  relexpxpnnidm  43944  relexpiidm  43945  relexpmulnn  43950  relexpaddss  43959  trclfvcom  43964  trclfvdecomr  43969  frege131d  44005  dssmap2d  44263  fundcmpsurbijinjpreimafv  47653  gricushgr  48163  prcof21a  49636