Theorem coeq1d 5841

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

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

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-br 5104  df-opab 5168  df-co 5664

This theorem is used by:  coeq12d  5844  fcof1oinvd  7294  domss2  9134  mapen  9139  mapfien  9378  hashfacen  14519  relexpsucnnr  15098  relexpsucnnl  15103  relexpsucr  15105  relexpsucrd  15106  relexpaddnn  15124  imasval  17597  cofuass  17978  cofulid  17979  setcinv  18179  catcisolem  18199  catciso  18200  yonedalem3b  18367  gsumvalx  18778  frmdup3lem  18975  symggrplem  18993  f1omvdco2  19575  symggen  19597  psgnunilem1  19620  gsumval3  20034  gsumzf1o  20039  znval  21748  znle2  21766  psrass1lem  22148  coe1add  22490  evls1fval  22544  evl1sca  22559  evl1var  22561  evls1var  22563  pf1mpf  22577  pf1ind  22580  tcphds  25459  dvnfval  26149  hocsubdir  32266  fcoinver  33077  fcobij  33191  cocnvf1o  33200  ccatws1f1olast  33394  symgfcoeu  33522  symgcom  33523  pmtrcnel2  33530  tocyc01  33558  cycpm2tr  33559  cycpmconjv  33582  cycpmconjslem1  33594  cycpmconjslem2  33595  cycpmconjs  33596  cyc3conja  33597  1arithidomlem2  33946  mplvrpmga  34055  mplvrpmrhm  34057  reprpmtf1o  35134  hgt750lemg  35162  subfacp1lem5  35763  mrsubffval  36086  mrsubfval  36087  mrsubrn  36092  elmrsubrn  36099  upixp  38479  ltrncoidN  41001  trlcoat  41596  trlcone  41601  cdlemg47a  41607  cdlemg47  41609  ltrnco4  41612  tendovalco  41638  tendoplcbv  41648  tendopl  41649  tendoplass  41656  tendo0pl  41664  tendoipl  41670  cdlemk45  41820  cdlemk53b  41829  cdlemk55a  41832  erngdvlem3  41863  erngdvlem3-rN  41871  tendocnv  41894  dvhvaddcbv  41962  dvhvaddval  41963  dvhvaddass  41970  dicvscacl  42064  cdlemn8  42077  dihordlem7b  42088  dihopelvalcpre  42121  aks6d1c6lem5  43043  relexp2  44517  relexpxpnnidm  44543  relexpiidm  44544  relexpmulnn  44549  relexpaddss  44558  trclfvcom  44563  trclfvdecomr  44568  frege131d  44604  dssmap2d  44862  fundcmpsurbijinjpreimafv  48307  gricushgr  48833  prcof21a  50317