Theorem coeq2d 5611

Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)

Hypothesis

Ref	Expression
coeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
coeq2d	⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

Proof of Theorem coeq2d

Step	Hyp	Ref	Expression
1		coeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		coeq2 5607	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∘ 𝐴) = (𝐶 ∘ 𝐵))

Syntax hints:   → wi 4   = wceq 1520   ∘ ccom 5439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-in 3861  df-ss 3869  df-br 4957  df-opab 5019  df-co 5444

This theorem is referenced by:  coeq12d  5613  f1ococnv1  6503  funcoeqres  6505  fcof1oinvd  6905  foeqcnvco  6912  fparlem3  7656  fparlem4  7657  mapen  8518  mapfien  8707  wemapwe  8995  hashfacen  13648  s1co  14019  pfxco  14024  relexpsucnnl  14213  relexpsucl  14214  relexpcnv  14216  relexpaddnn  14232  relexpaddg  14234  prdsval  16545  isofval  16844  cofuass  16976  cofurid  16978  fucid  17058  setcinv  17167  catcisolem  17183  curf2ndf  17314  pwsco2mhm  17798  symggrp  18247  f1omvdco2  18295  psgnunilem1  18340  efginvrel2  18568  efginvrel1  18569  vrgpinv  18610  frgpuplem  18613  gsumval3  18736  gsumzf1o  18741  psrass1lem  19833  mpfrcl  19973  evlsval  19974  selvffval  20000  selvfval  20001  evls1fval  20153  evl1fval  20161  pf1mpf  20185  pf1ind  20188  ofco2  20732  qtophmeo  22097  ustssco  22494  utop2nei  22530  neipcfilu  22576  tngds  22928  elovolmr  23748  ovoliunlem3  23776  uniioombllem2  23855  hoddi  29446  fcoinver  30022  fmptco1f1o  30041  fcobij  30119  symgfcoeu  30355  symgcom  30356  tocycf  30370  cycpmconjvlem  30383  cycpmconjv  30384  cycpmconjslem1  30392  cycpmconjslem2  30393  cycpmconjs  30394  cyc3conja  30395  smatfval  30631  eulerpartlemgv  31204  eulerpartlemn  31212  eulerpart  31213  sseqval  31219  reprpmtf1o  31470  erdsze2lem2  32015  cvmliftlem10  32105  mrsubval  32309  dfpo2  32544  ftc1anclem8  34451  cocnv  34478  ltrncoidN  36745  trlcoabs2N  37339  cdlemg47a  37351  cdlemg46  37352  cdlemg47  37353  ltrnco4  37356  tendovalco  37382  tendoplcbv  37392  tendopl  37393  tendoplass  37400  cdlemi2  37436  cdlemk2  37449  cdlemk4  37451  cdlemk8  37455  cdlemkuu  37512  cdlemk53  37574  cdlemk54  37575  cdlemk55a  37576  erngdvlem3  37607  erngdvlem3-rN  37615  tendocnv  37638  tendospcanN  37640  dvhvaddcbv  37706  dvhvaddval  37707  dvhvaddass  37714  dvhvscacbv  37715  dvhvscaval  37716  dvhopvsca  37719  dvhlveclem  37725  dvhopspN  37732  diblss  37787  cdlemn8  37821  dihopelvalcpre  37865  dihmeetlem1N  37907  dihglblem5apreN  37908  dih1dimatlem0  37945  dihjatcclem4  38038  diophrw  38791  eldioph2  38794  relexpaddss  39499  trclfvcom  39504  frege131d  39545  fsovrfovd  39791  hoicvrrex  42334  ovnlecvr  42336  ovncvrrp  42342  ovn0lem  42343  ovnsubaddlem1  42348  ovnsubadd  42350  ovnhoilem1  42379  ovnhoi  42381  ovnlecvr2  42388  ovncvr2  42389  hspmbl  42407  ovnovollem1  42434  ovnovollem3  42436