Theorem coeq1d 5807

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

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3915  df-br 5096  df-opab 5158  df-co 5630

This theorem is referenced by:  coeq12d  5810  fcof1oinvd  7236  domss2  9060  mapen  9065  mapfien  9303  hashfacen  14368  relexpsucnnr  14939  relexpsucnnl  14944  relexpsucr  14946  relexpsucrd  14947  relexpaddnn  14965  imasval  17423  cofuass  17804  cofulid  17805  setcinv  18005  catcisolem  18025  catciso  18026  yonedalem3b  18193  gsumvalx  18592  frmdup3lem  18782  symggrplem  18800  f1omvdco2  19368  symggen  19390  psgnunilem1  19413  gsumval3  19827  gsumzf1o  19832  znval  21481  znle2  21499  psrass1lem  21879  coe1add  22197  evls1fval  22254  evl1sca  22269  evl1var  22271  evls1var  22273  pf1mpf  22287  pf1ind  22290  tcphds  25178  dvnfval  25871  hocsubdir  31786  fcoinver  32605  fcobij  32727  cocnvf1o  32736  ccatws1f1olast  32962  symgfcoeu  33092  symgcom  33093  pmtrcnel2  33100  tocyc01  33128  cycpm2tr  33129  cycpmconjv  33152  cycpmconjslem1  33164  cycpmconjslem2  33165  cycpmconjs  33166  cyc3conja  33167  1arithidomlem2  33545  mplvrpmga  33638  mplvrpmrhm  33640  reprpmtf1o  34711  hgt750lemg  34739  subfacp1lem5  35300  mrsubffval  35623  mrsubfval  35624  mrsubrn  35629  elmrsubrn  35636  upixp  37842  ltrncoidN  40300  trlcoat  40895  trlcone  40900  cdlemg47a  40906  cdlemg47  40908  ltrnco4  40911  tendovalco  40937  tendoplcbv  40947  tendopl  40948  tendoplass  40955  tendo0pl  40963  tendoipl  40969  cdlemk45  41119  cdlemk53b  41128  cdlemk55a  41131  erngdvlem3  41162  erngdvlem3-rN  41170  tendocnv  41193  dvhvaddcbv  41261  dvhvaddval  41262  dvhvaddass  41269  dicvscacl  41363  cdlemn8  41376  dihordlem7b  41387  dihopelvalcpre  41420  aks6d1c6lem5  42343  relexp2  43834  relexpxpnnidm  43860  relexpiidm  43861  relexpmulnn  43866  relexpaddss  43875  trclfvcom  43880  trclfvdecomr  43885  frege131d  43921  dssmap2d  44179  fundcmpsurbijinjpreimafv  47569  gricushgr  48079  prcof21a  49552