Theorem coeq1d 5796

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

Syntax hints:   → wi 4   = wceq 1541   ∘ ccom 5615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914  df-br 5087  df-opab 5149  df-co 5620

This theorem is referenced by:  coeq12d  5799  fcof1oinvd  7222  domss2  9044  mapen  9049  mapfien  9287  hashfacen  14356  relexpsucnnr  14927  relexpsucnnl  14932  relexpsucr  14934  relexpsucrd  14935  relexpaddnn  14953  imasval  17410  cofuass  17791  cofulid  17792  setcinv  17992  catcisolem  18012  catciso  18013  yonedalem3b  18180  gsumvalx  18579  frmdup3lem  18769  symggrplem  18787  f1omvdco2  19355  symggen  19377  psgnunilem1  19400  gsumval3  19814  gsumzf1o  19819  znval  21467  znle2  21485  psrass1lem  21864  coe1add  22173  evls1fval  22229  evl1sca  22244  evl1var  22246  evls1var  22248  pf1mpf  22262  pf1ind  22265  tcphds  25153  dvnfval  25846  hocsubdir  31757  fcoinver  32576  fcobij  32695  cocnvf1o  32704  ccatws1f1olast  32925  symgfcoeu  33043  symgcom  33044  pmtrcnel2  33051  tocyc01  33079  cycpm2tr  33080  cycpmconjv  33103  cycpmconjslem1  33115  cycpmconjslem2  33116  cycpmconjs  33117  cyc3conja  33118  1arithidomlem2  33493  mplvrpmga  33567  mplvrpmrhm  33569  reprpmtf1o  34631  hgt750lemg  34659  subfacp1lem5  35220  mrsubffval  35543  mrsubfval  35544  mrsubrn  35549  elmrsubrn  35556  upixp  37769  ltrncoidN  40167  trlcoat  40762  trlcone  40767  cdlemg47a  40773  cdlemg47  40775  ltrnco4  40778  tendovalco  40804  tendoplcbv  40814  tendopl  40815  tendoplass  40822  tendo0pl  40830  tendoipl  40836  cdlemk45  40986  cdlemk53b  40995  cdlemk55a  40998  erngdvlem3  41029  erngdvlem3-rN  41037  tendocnv  41060  dvhvaddcbv  41128  dvhvaddval  41129  dvhvaddass  41136  dicvscacl  41230  cdlemn8  41243  dihordlem7b  41254  dihopelvalcpre  41287  aks6d1c6lem5  42210  relexp2  43710  relexpxpnnidm  43736  relexpiidm  43737  relexpmulnn  43742  relexpaddss  43751  trclfvcom  43756  trclfvdecomr  43761  frege131d  43797  dssmap2d  44055  fundcmpsurbijinjpreimafv  47438  gricushgr  47948  prcof21a  49423