Theorem coeq1d 5845

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

Syntax hints:   → wi 4   = wceq 1567   ∘ ccom 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-br 5111  df-opab 5175  df-co 5668

This theorem is referenced by:  coeq12d  5848  fcof1oinvd  7289  domss2  9120  mapen  9125  mapfien  9364  hashfacen  14487  relexpsucnnr  15058  relexpsucnnl  15063  relexpsucr  15065  relexpsucrd  15066  relexpaddnn  15084  imasval  17561  cofuass  17942  cofulid  17943  setcinv  18143  catcisolem  18163  catciso  18164  yonedalem3b  18331  gsumvalx  18730  frmdup3lem  18921  symggrplem  18939  f1omvdco2  19514  symggen  19536  psgnunilem1  19559  gsumval3  19973  gsumzf1o  19978  znval  21650  znle2  21668  psrass1lem  22048  coe1add  22390  evls1fval  22444  evl1sca  22459  evl1var  22461  evls1var  22463  pf1mpf  22477  pf1ind  22480  tcphds  25355  dvnfval  26046  hocsubdir  32074  fcoinver  32886  fcobij  33002  cocnvf1o  33011  ccatws1f1olast  33209  symgfcoeu  33339  symgcom  33340  pmtrcnel2  33347  tocyc01  33375  cycpm2tr  33376  cycpmconjv  33399  cycpmconjslem1  33411  cycpmconjslem2  33412  cycpmconjs  33413  cyc3conja  33414  1arithidomlem2  33767  mplvrpmga  33876  mplvrpmrhm  33878  reprpmtf1o  34954  hgt750lemg  34982  subfacp1lem5  35571  mrsubffval  35894  mrsubfval  35895  mrsubrn  35900  elmrsubrn  35907  upixp  38263  ltrncoidN  40787  trlcoat  41382  trlcone  41387  cdlemg47a  41393  cdlemg47  41395  ltrnco4  41398  tendovalco  41424  tendoplcbv  41434  tendopl  41435  tendoplass  41442  tendo0pl  41450  tendoipl  41456  cdlemk45  41606  cdlemk53b  41615  cdlemk55a  41618  erngdvlem3  41649  erngdvlem3-rN  41657  tendocnv  41680  dvhvaddcbv  41748  dvhvaddval  41749  dvhvaddass  41756  dicvscacl  41850  cdlemn8  41863  dihordlem7b  41874  dihopelvalcpre  41907  aks6d1c6lem5  42829  relexp2  44290  relexpxpnnidm  44316  relexpiidm  44317  relexpmulnn  44322  relexpaddss  44331  trclfvcom  44336  trclfvdecomr  44341  frege131d  44377  dssmap2d  44635  fundcmpsurbijinjpreimafv  48040  gricushgr  48566  prcof21a  50049