Theorem coeq1d 5849

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923  df-br 5112  df-opab 5176  df-co 5672

This theorem is used by:  coeq12d  5852  fcof1oinvd  7297  domss2  9127  mapen  9132  mapfien  9371  hashfacen  14505  relexpsucnnr  15082  relexpsucnnl  15087  relexpsucr  15089  relexpsucrd  15090  relexpaddnn  15108  imasval  17583  cofuass  17964  cofulid  17965  setcinv  18165  catcisolem  18185  catciso  18186  yonedalem3b  18353  gsumvalx  18756  frmdup3lem  18949  symggrplem  18967  f1omvdco2  19542  symggen  19564  psgnunilem1  19587  gsumval3  20001  gsumzf1o  20006  znval  21715  znle2  21733  psrass1lem  22113  coe1add  22455  evls1fval  22509  evl1sca  22524  evl1var  22526  evls1var  22528  pf1mpf  22542  pf1ind  22545  tcphds  25421  dvnfval  26112  hocsubdir  32184  fcoinver  32996  fcobij  33111  cocnvf1o  33120  ccatws1f1olast  33314  symgfcoeu  33442  symgcom  33443  pmtrcnel2  33450  tocyc01  33478  cycpm2tr  33479  cycpmconjv  33502  cycpmconjslem1  33514  cycpmconjslem2  33515  cycpmconjs  33516  cyc3conja  33517  1arithidomlem2  33866  mplvrpmga  33975  mplvrpmrhm  33977  reprpmtf1o  35054  hgt750lemg  35082  subfacp1lem5  35689  mrsubffval  36012  mrsubfval  36013  mrsubrn  36018  elmrsubrn  36025  upixp  38413  ltrncoidN  40935  trlcoat  41530  trlcone  41535  cdlemg47a  41541  cdlemg47  41543  ltrnco4  41546  tendovalco  41572  tendoplcbv  41582  tendopl  41583  tendoplass  41590  tendo0pl  41598  tendoipl  41604  cdlemk45  41754  cdlemk53b  41763  cdlemk55a  41766  erngdvlem3  41797  erngdvlem3-rN  41805  tendocnv  41828  dvhvaddcbv  41896  dvhvaddval  41897  dvhvaddass  41904  dicvscacl  41998  cdlemn8  42011  dihordlem7b  42022  dihopelvalcpre  42055  aks6d1c6lem5  42977  relexp2  44436  relexpxpnnidm  44462  relexpiidm  44463  relexpmulnn  44468  relexpaddss  44477  trclfvcom  44482  trclfvdecomr  44487  frege131d  44523  dssmap2d  44781  fundcmpsurbijinjpreimafv  48189  gricushgr  48715  prcof21a  50202