Theorem coeq1d 5850

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∘ ccom 5662

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5109  df-opab 5174  df-co 5667

This theorem is used by:  coeq12d  5853  fcof1oinvd  7332  domss2  9193  mapen  9198  mapfien  9437  hashfacen  14640  relexpsucnnr  15221  relexpsucnnl  15226  relexpsucr  15228  relexpsucrd  15229  relexpaddnn  15247  imasval  17733  cofuass  18114  cofulid  18115  setcinv  18315  catcisolem  18335  catciso  18336  yonedalem3b  18503  gsumvalx  18915  frmdup3lem  19112  symggrplem  19130  f1omvdco2  19713  symggen  19735  psgnunilem1  19758  gsumval3  20172  gsumzf1o  20177  znval  21896  znle2  21914  psrass1lem  22296  coe1add  22638  evls1fval  22692  evl1sca  22707  evl1var  22709  evls1var  22711  pf1mpf  22725  pf1ind  22728  tcphds  25607  dvnfval  26297  hocsubdir  32444  fcoinver  33296  fcobij  33408  cocnvf1o  33417  ccatws1f1olast  33611  symgfcoeu  33742  symgcom  33743  pmtrcnel2  33750  tocyc01  33778  cycpm2tr  33779  cycpmconjv  33802  cycpmconjslem1  33814  cycpmconjslem2  33815  cycpmconjs  33816  cyc3conja  33817  1arithidomlem2  34172  mplvrpmga  34288  mplvrpmrhm  34290  reprpmtf1o  35366  hgt750lemg  35394  subfacp1lem5  36157  mrsubffval  36480  mrsubfval  36481  mrsubrn  36486  elmrsubrn  36493  coss2b  38218  upixp  38931  ltrncoidN  41451  trlcoat  42046  trlcone  42051  cdlemg47a  42057  cdlemg47  42059  ltrnco4  42062  tendovalco  42088  tendoplcbv  42098  tendopl  42099  tendoplass  42106  tendo0pl  42114  tendoipl  42120  cdlemk45  42270  cdlemk53b  42279  cdlemk55a  42282  erngdvlem3  42313  erngdvlem3-rN  42321  tendocnv  42344  dvhvaddcbv  42412  dvhvaddval  42413  dvhvaddass  42420  dicvscacl  42514  cdlemn8  42527  dihordlem7b  42538  dihopelvalcpre  42571  aks6d1c6lem5  43493  relexp2  44938  relexpxpnnidm  44964  relexpiidm  44965  relexpmulnn  44970  relexpaddss  44979  trclfvcom  44984  trclfvdecomr  44989  frege131d  45025  dssmap2d  45283  fundcmpsurbijinjpreimafv  48762  gricushgr  49288  cofu1stfix  50543  prcof21a  50857