Theorem coeq1d 5862

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

Syntax hints:   → wi 4   = wceq 1542   ∘ ccom 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-co 5686

This theorem is referenced by:  coeq12d  5865  fcof1oinvd  7291  domss2  9136  mapen  9141  mapfien  9403  hashfacen  14413  hashfacenOLD  14414  relexpsucnnr  14972  relexpsucnnl  14977  relexpsucr  14979  relexpsucrd  14980  relexpaddnn  14998  imasval  17457  cofuass  17839  cofulid  17840  setcinv  18040  catcisolem  18060  catciso  18061  yonedalem3b  18232  gsumvalx  18595  frmdup3lem  18747  symggrplem  18765  f1omvdco2  19316  symggen  19338  psgnunilem1  19361  gsumval3  19775  gsumzf1o  19780  znval  21087  znle2  21109  psrass1lemOLD  21493  psrass1lem  21496  coe1add  21786  evls1fval  21838  evl1sca  21853  evl1var  21855  evls1var  21857  pf1mpf  21871  pf1ind  21874  tcphds  24748  dvnfval  25439  hocsubdir  31069  fcoinver  31866  fcobij  31978  symgfcoeu  32274  symgcom  32275  pmtrcnel2  32282  tocyc01  32308  cycpm2tr  32309  cycpmconjv  32332  cycpmconjslem1  32344  cycpmconjslem2  32345  cycpmconjs  32346  cyc3conja  32347  reprpmtf1o  33669  hgt750lemg  33697  subfacp1lem5  34206  mrsubffval  34529  mrsubfval  34530  mrsubrn  34535  elmrsubrn  34542  upixp  36645  ltrncoidN  39047  trlcoat  39642  trlcone  39647  cdlemg47a  39653  cdlemg47  39655  ltrnco4  39658  tendovalco  39684  tendoplcbv  39694  tendopl  39695  tendoplass  39702  tendo0pl  39710  tendoipl  39716  cdlemk45  39866  cdlemk53b  39875  cdlemk55a  39878  erngdvlem3  39909  erngdvlem3-rN  39917  tendocnv  39940  dvhvaddcbv  40008  dvhvaddval  40009  dvhvaddass  40016  dicvscacl  40110  cdlemn8  40123  dihordlem7b  40134  dihopelvalcpre  40167  relexp2  42476  relexpxpnnidm  42502  relexpiidm  42503  relexpmulnn  42508  relexpaddss  42517  trclfvcom  42522  trclfvdecomr  42527  frege131d  42563  dssmap2d  42821  fundcmpsurbijinjpreimafv  46123  isomushgr  46542