Theorem coeq1d 5816

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

Syntax hints:   → wi 4   = wceq 1542   ∘ ccom 5635

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-br 5086  df-opab 5148  df-co 5640

This theorem is referenced by:  coeq12d  5819  fcof1oinvd  7248  domss2  9074  mapen  9079  mapfien  9321  hashfacen  14416  relexpsucnnr  14987  relexpsucnnl  14992  relexpsucr  14994  relexpsucrd  14995  relexpaddnn  15013  imasval  17475  cofuass  17856  cofulid  17857  setcinv  18057  catcisolem  18077  catciso  18078  yonedalem3b  18245  gsumvalx  18644  frmdup3lem  18834  symggrplem  18852  f1omvdco2  19423  symggen  19445  psgnunilem1  19468  gsumval3  19882  gsumzf1o  19887  znval  21515  znle2  21533  psrass1lem  21912  coe1add  22229  evls1fval  22284  evl1sca  22299  evl1var  22301  evls1var  22303  pf1mpf  22317  pf1ind  22320  tcphds  25198  dvnfval  25889  hocsubdir  31856  fcoinver  32674  fcobij  32793  cocnvf1o  32802  ccatws1f1olast  33012  symgfcoeu  33143  symgcom  33144  pmtrcnel2  33151  tocyc01  33179  cycpm2tr  33180  cycpmconjv  33203  cycpmconjslem1  33215  cycpmconjslem2  33216  cycpmconjs  33217  cyc3conja  33218  1arithidomlem2  33596  mplvrpmga  33689  mplvrpmrhm  33691  reprpmtf1o  34770  hgt750lemg  34798  subfacp1lem5  35366  mrsubffval  35689  mrsubfval  35690  mrsubrn  35695  elmrsubrn  35702  upixp  38050  ltrncoidN  40574  trlcoat  41169  trlcone  41174  cdlemg47a  41180  cdlemg47  41182  ltrnco4  41185  tendovalco  41211  tendoplcbv  41221  tendopl  41222  tendoplass  41229  tendo0pl  41237  tendoipl  41243  cdlemk45  41393  cdlemk53b  41402  cdlemk55a  41405  erngdvlem3  41436  erngdvlem3-rN  41444  tendocnv  41467  dvhvaddcbv  41535  dvhvaddval  41536  dvhvaddass  41543  dicvscacl  41637  cdlemn8  41650  dihordlem7b  41661  dihopelvalcpre  41694  aks6d1c6lem5  42616  relexp2  44104  relexpxpnnidm  44130  relexpiidm  44131  relexpmulnn  44136  relexpaddss  44145  trclfvcom  44150  trclfvdecomr  44155  frege131d  44191  dssmap2d  44449  fundcmpsurbijinjpreimafv  47867  gricushgr  48393  prcof21a  49866