Theorem coeq1d 5803

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

Syntax hints:   → wi 4   = wceq 1547   ∘ ccom 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900  df-br 5073  df-opab 5135  df-co 5627

This theorem is referenced by:  coeq12d  5806  fcof1oinvd  7237  domss2  9064  mapen  9069  mapfien  9311  hashfacen  14407  relexpsucnnr  14978  relexpsucnnl  14983  relexpsucr  14985  relexpsucrd  14986  relexpaddnn  15004  imasval  17466  cofuass  17847  cofulid  17848  setcinv  18048  catcisolem  18068  catciso  18069  yonedalem3b  18236  gsumvalx  18635  frmdup3lem  18825  symggrplem  18843  f1omvdco2  19414  symggen  19436  psgnunilem1  19459  gsumval3  19873  gsumzf1o  19878  znval  21510  znle2  21528  psrass1lem  21908  coe1add  22250  evls1fval  22305  evl1sca  22320  evl1var  22322  evls1var  22324  pf1mpf  22338  pf1ind  22341  tcphds  25216  dvnfval  25907  hocsubdir  31874  fcoinver  32693  fcobij  32812  cocnvf1o  32821  ccatws1f1olast  33031  symgfcoeu  33163  symgcom  33164  pmtrcnel2  33171  tocyc01  33199  cycpm2tr  33200  cycpmconjv  33223  cycpmconjslem1  33235  cycpmconjslem2  33236  cycpmconjs  33237  cyc3conja  33238  1arithidomlem2  33619  mplvrpmga  33729  mplvrpmrhm  33731  reprpmtf1o  34810  hgt750lemg  34838  subfacp1lem5  35412  mrsubffval  35735  mrsubfval  35736  mrsubrn  35741  elmrsubrn  35748  upixp  38096  ltrncoidN  40620  trlcoat  41215  trlcone  41220  cdlemg47a  41226  cdlemg47  41228  ltrnco4  41231  tendovalco  41257  tendoplcbv  41267  tendopl  41268  tendoplass  41275  tendo0pl  41283  tendoipl  41289  cdlemk45  41439  cdlemk53b  41448  cdlemk55a  41451  erngdvlem3  41482  erngdvlem3-rN  41490  tendocnv  41513  dvhvaddcbv  41581  dvhvaddval  41582  dvhvaddass  41589  dicvscacl  41683  cdlemn8  41696  dihordlem7b  41707  dihopelvalcpre  41740  aks6d1c6lem5  42662  relexp2  44121  relexpxpnnidm  44147  relexpiidm  44148  relexpmulnn  44153  relexpaddss  44162  trclfvcom  44167  trclfvdecomr  44172  frege131d  44208  dssmap2d  44466  fundcmpsurbijinjpreimafv  47882  gricushgr  48408  prcof21a  49881