Theorem coeq1d 5874

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

Syntax hints:   → wi 4   = wceq 1536   ∘ ccom 5692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-br 5148  df-opab 5210  df-co 5697

This theorem is referenced by:  coeq12d  5877  fcof1oinvd  7312  domss2  9174  mapen  9179  mapfien  9445  hashfacen  14489  relexpsucnnr  15060  relexpsucnnl  15065  relexpsucr  15067  relexpsucrd  15068  relexpaddnn  15086  imasval  17557  cofuass  17939  cofulid  17940  setcinv  18143  catcisolem  18163  catciso  18164  yonedalem3b  18335  gsumvalx  18701  frmdup3lem  18891  symggrplem  18909  f1omvdco2  19480  symggen  19502  psgnunilem1  19525  gsumval3  19939  gsumzf1o  19944  znval  21567  znle2  21589  psrass1lem  21969  coe1add  22282  evls1fval  22338  evl1sca  22353  evl1var  22355  evls1var  22357  pf1mpf  22371  pf1ind  22374  tcphds  25278  dvnfval  25972  hocsubdir  31813  fcoinver  32623  fcobij  32739  ccatws1f1olast  32921  symgfcoeu  33084  symgcom  33085  pmtrcnel2  33092  tocyc01  33120  cycpm2tr  33121  cycpmconjv  33144  cycpmconjslem1  33156  cycpmconjslem2  33157  cycpmconjs  33158  cyc3conja  33159  1arithidomlem2  33543  reprpmtf1o  34619  hgt750lemg  34647  subfacp1lem5  35168  mrsubffval  35491  mrsubfval  35492  mrsubrn  35497  elmrsubrn  35504  upixp  37715  ltrncoidN  40110  trlcoat  40705  trlcone  40710  cdlemg47a  40716  cdlemg47  40718  ltrnco4  40721  tendovalco  40747  tendoplcbv  40757  tendopl  40758  tendoplass  40765  tendo0pl  40773  tendoipl  40779  cdlemk45  40929  cdlemk53b  40938  cdlemk55a  40941  erngdvlem3  40972  erngdvlem3-rN  40980  tendocnv  41003  dvhvaddcbv  41071  dvhvaddval  41072  dvhvaddass  41079  dicvscacl  41173  cdlemn8  41186  dihordlem7b  41197  dihopelvalcpre  41230  aks6d1c6lem5  42158  relexp2  43666  relexpxpnnidm  43692  relexpiidm  43693  relexpmulnn  43698  relexpaddss  43707  trclfvcom  43712  trclfvdecomr  43717  frege131d  43753  dssmap2d  44011  fundcmpsurbijinjpreimafv  47331  gricushgr  47823