Theorem coeq1d 5861

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-br 5149  df-opab 5211  df-co 5685

This theorem is referenced by:  coeq12d  5864  fcof1oinvd  7290  domss2  9135  mapen  9140  mapfien  9402  hashfacen  14412  hashfacenOLD  14413  relexpsucnnr  14971  relexpsucnnl  14976  relexpsucr  14978  relexpsucrd  14979  relexpaddnn  14997  imasval  17456  cofuass  17838  cofulid  17839  setcinv  18039  catcisolem  18059  catciso  18060  yonedalem3b  18231  gsumvalx  18594  frmdup3lem  18746  symggrplem  18764  f1omvdco2  19315  symggen  19337  psgnunilem1  19360  gsumval3  19774  gsumzf1o  19779  znval  21086  znle2  21108  psrass1lemOLD  21492  psrass1lem  21495  coe1add  21785  evls1fval  21837  evl1sca  21852  evl1var  21854  evls1var  21856  pf1mpf  21870  pf1ind  21873  tcphds  24747  dvnfval  25438  hocsubdir  31033  fcoinver  31830  fcobij  31942  symgfcoeu  32238  symgcom  32239  pmtrcnel2  32246  tocyc01  32272  cycpm2tr  32273  cycpmconjv  32296  cycpmconjslem1  32308  cycpmconjslem2  32309  cycpmconjs  32310  cyc3conja  32311  reprpmtf1o  33633  hgt750lemg  33661  subfacp1lem5  34170  mrsubffval  34493  mrsubfval  34494  mrsubrn  34499  elmrsubrn  34506  upixp  36592  ltrncoidN  38994  trlcoat  39589  trlcone  39594  cdlemg47a  39600  cdlemg47  39602  ltrnco4  39605  tendovalco  39631  tendoplcbv  39641  tendopl  39642  tendoplass  39649  tendo0pl  39657  tendoipl  39663  cdlemk45  39813  cdlemk53b  39822  cdlemk55a  39825  erngdvlem3  39856  erngdvlem3-rN  39864  tendocnv  39887  dvhvaddcbv  39955  dvhvaddval  39956  dvhvaddass  39963  dicvscacl  40057  cdlemn8  40070  dihordlem7b  40081  dihopelvalcpre  40114  relexp2  42418  relexpxpnnidm  42444  relexpiidm  42445  relexpmulnn  42450  relexpaddss  42459  trclfvcom  42464  trclfvdecomr  42469  frege131d  42505  dssmap2d  42763  fundcmpsurbijinjpreimafv  46065  isomushgr  46484