Theorem coeq1d 5886

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

Syntax hints:   → wi 4   = wceq 1537   ∘ ccom 5704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-co 5709

This theorem is referenced by:  coeq12d  5889  fcof1oinvd  7329  domss2  9202  mapen  9207  mapfien  9477  hashfacen  14503  relexpsucnnr  15074  relexpsucnnl  15079  relexpsucr  15081  relexpsucrd  15082  relexpaddnn  15100  imasval  17571  cofuass  17953  cofulid  17954  setcinv  18157  catcisolem  18177  catciso  18178  yonedalem3b  18349  gsumvalx  18714  frmdup3lem  18901  symggrplem  18919  f1omvdco2  19490  symggen  19512  psgnunilem1  19535  gsumval3  19949  gsumzf1o  19954  znval  21573  znle2  21595  psrass1lem  21975  coe1add  22288  evls1fval  22344  evl1sca  22359  evl1var  22361  evls1var  22363  pf1mpf  22377  pf1ind  22380  tcphds  25284  dvnfval  25978  hocsubdir  31817  fcoinver  32626  fcobij  32736  ccatws1f1olast  32919  symgfcoeu  33075  symgcom  33076  pmtrcnel2  33083  tocyc01  33111  cycpm2tr  33112  cycpmconjv  33135  cycpmconjslem1  33147  cycpmconjslem2  33148  cycpmconjs  33149  cyc3conja  33150  1arithidomlem2  33529  reprpmtf1o  34603  hgt750lemg  34631  subfacp1lem5  35152  mrsubffval  35475  mrsubfval  35476  mrsubrn  35481  elmrsubrn  35488  upixp  37689  ltrncoidN  40085  trlcoat  40680  trlcone  40685  cdlemg47a  40691  cdlemg47  40693  ltrnco4  40696  tendovalco  40722  tendoplcbv  40732  tendopl  40733  tendoplass  40740  tendo0pl  40748  tendoipl  40754  cdlemk45  40904  cdlemk53b  40913  cdlemk55a  40916  erngdvlem3  40947  erngdvlem3-rN  40955  tendocnv  40978  dvhvaddcbv  41046  dvhvaddval  41047  dvhvaddass  41054  dicvscacl  41148  cdlemn8  41161  dihordlem7b  41172  dihopelvalcpre  41205  aks6d1c6lem5  42134  relexp2  43639  relexpxpnnidm  43665  relexpiidm  43666  relexpmulnn  43671  relexpaddss  43680  trclfvcom  43685  trclfvdecomr  43690  frege131d  43726  dssmap2d  43984  fundcmpsurbijinjpreimafv  47281  gricushgr  47770