Theorem coeq1d 5828

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

Syntax hints:   → wi 4   = wceq 1540   ∘ ccom 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-co 5650

This theorem is referenced by:  coeq12d  5831  fcof1oinvd  7271  domss2  9106  mapen  9111  mapfien  9366  hashfacen  14426  relexpsucnnr  14998  relexpsucnnl  15003  relexpsucr  15005  relexpsucrd  15006  relexpaddnn  15024  imasval  17481  cofuass  17858  cofulid  17859  setcinv  18059  catcisolem  18079  catciso  18080  yonedalem3b  18247  gsumvalx  18610  frmdup3lem  18800  symggrplem  18818  f1omvdco2  19385  symggen  19407  psgnunilem1  19430  gsumval3  19844  gsumzf1o  19849  znval  21452  znle2  21470  psrass1lem  21848  coe1add  22157  evls1fval  22213  evl1sca  22228  evl1var  22230  evls1var  22232  pf1mpf  22246  pf1ind  22249  tcphds  25138  dvnfval  25831  hocsubdir  31721  fcoinver  32540  fcobij  32652  ccatws1f1olast  32881  symgfcoeu  33046  symgcom  33047  pmtrcnel2  33054  tocyc01  33082  cycpm2tr  33083  cycpmconjv  33106  cycpmconjslem1  33118  cycpmconjslem2  33119  cycpmconjs  33120  cyc3conja  33121  1arithidomlem2  33514  reprpmtf1o  34624  hgt750lemg  34652  subfacp1lem5  35178  mrsubffval  35501  mrsubfval  35502  mrsubrn  35507  elmrsubrn  35514  upixp  37730  ltrncoidN  40129  trlcoat  40724  trlcone  40729  cdlemg47a  40735  cdlemg47  40737  ltrnco4  40740  tendovalco  40766  tendoplcbv  40776  tendopl  40777  tendoplass  40784  tendo0pl  40792  tendoipl  40798  cdlemk45  40948  cdlemk53b  40957  cdlemk55a  40960  erngdvlem3  40991  erngdvlem3-rN  40999  tendocnv  41022  dvhvaddcbv  41090  dvhvaddval  41091  dvhvaddass  41098  dicvscacl  41192  cdlemn8  41205  dihordlem7b  41216  dihopelvalcpre  41249  aks6d1c6lem5  42172  relexp2  43673  relexpxpnnidm  43699  relexpiidm  43700  relexpmulnn  43705  relexpaddss  43714  trclfvcom  43719  trclfvdecomr  43724  frege131d  43760  dssmap2d  44018  fundcmpsurbijinjpreimafv  47412  gricushgr  47921  prcof21a  49384