Theorem coeq1d 5847

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

Syntax hints:   → wi 4   = wceq 1570   ∘ ccom 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-br 5110  df-opab 5174  df-co 5670

This theorem is referenced by:  coeq12d  5850  fcof1oinvd  7291  domss2  9120  mapen  9125  mapfien  9364  hashfacen  14487  relexpsucnnr  15058  relexpsucnnl  15063  relexpsucr  15065  relexpsucrd  15066  relexpaddnn  15084  imasval  17560  cofuass  17941  cofulid  17942  setcinv  18142  catcisolem  18162  catciso  18163  yonedalem3b  18330  gsumvalx  18729  frmdup3lem  18920  symggrplem  18938  f1omvdco2  19513  symggen  19535  psgnunilem1  19558  gsumval3  19972  gsumzf1o  19977  znval  21685  znle2  21703  psrass1lem  22083  coe1add  22425  evls1fval  22479  evl1sca  22494  evl1var  22496  evls1var  22498  pf1mpf  22512  pf1ind  22515  tcphds  25390  dvnfval  26081  hocsubdir  32137  fcoinver  32949  fcobij  33065  cocnvf1o  33074  ccatws1f1olast  33272  symgfcoeu  33402  symgcom  33403  pmtrcnel2  33410  tocyc01  33438  cycpm2tr  33439  cycpmconjv  33462  cycpmconjslem1  33474  cycpmconjslem2  33475  cycpmconjs  33476  cyc3conja  33477  1arithidomlem2  33826  mplvrpmga  33935  mplvrpmrhm  33937  reprpmtf1o  35013  hgt750lemg  35041  subfacp1lem5  35676  mrsubffval  35999  mrsubfval  36000  mrsubrn  36005  elmrsubrn  36012  upixp  38380  ltrncoidN  40902  trlcoat  41497  trlcone  41502  cdlemg47a  41508  cdlemg47  41510  ltrnco4  41513  tendovalco  41539  tendoplcbv  41549  tendopl  41550  tendoplass  41557  tendo0pl  41565  tendoipl  41571  cdlemk45  41721  cdlemk53b  41730  cdlemk55a  41733  erngdvlem3  41764  erngdvlem3-rN  41772  tendocnv  41795  dvhvaddcbv  41863  dvhvaddval  41864  dvhvaddass  41871  dicvscacl  41965  cdlemn8  41978  dihordlem7b  41989  dihopelvalcpre  42022  aks6d1c6lem5  42944  relexp2  44403  relexpxpnnidm  44429  relexpiidm  44430  relexpmulnn  44435  relexpaddss  44444  trclfvcom  44449  trclfvdecomr  44454  frege131d  44490  dssmap2d  44748  fundcmpsurbijinjpreimafv  48156  gricushgr  48682  prcof21a  50169