Theorem coeq2d 5804

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

Syntax hints:   → wi 4   = wceq 1547   ∘ ccom 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900  df-br 5073  df-opab 5135  df-co 5627

This theorem is referenced by:  coeq12d  5806  dfpo2  6247  f1ococnv1  6796  funcoeqres  6798  fcof1oinvd  7237  foeqcnvco  7244  f1ofvswap  7250  coof  7644  fparlem3  8053  fparlem4  8054  offsplitfpar  8058  csbwrecsg  8258  mapen  9069  mapfien  9311  wemapwe  9609  hashfacen  14407  s1co  14786  pfxco  14791  relexpsucnnl  14983  relexpsucl  14984  relexpsucld  14987  relexpcnv  14988  relexpaddnn  15004  relexpaddg  15006  prdsval  17409  isofval  17715  cofuass  17847  cofurid  17849  fucid  17932  setcinv  18048  catcisolem  18068  curf2ndf  18204  pwsco2mhm  18792  symggrplem  18843  smndex1igid  18865  smndex1igidOLD  18866  f1omvdco2  19414  psgnunilem1  19459  efginvrel2  19693  efginvrel1  19694  vrgpinv  19735  frgpuplem  19738  gsumval3  19873  gsumzf1o  19878  psrass1lem  21908  mpfrcl  22061  evlsval  22062  selvval  22096  mhmcoaddmpl  22099  rhmcomulmpl  22100  evls1fval  22305  evl1fval  22314  pf1mpf  22338  pf1ind  22341  rhmmpl  22366  rhmply1vr1  22370  rhmply1vsca  22371  ofco2  22434  qtophmeo  23800  ustssco  24198  utop2nei  24233  neipcfilu  24278  tngds  24631  elovolmr  25461  ovoliunlem3  25489  uniioombllem2  25568  hoddi  32079  fcoinver  32693  fmptco1f1o  32725  fcobij  32812  cocnvf1o  32821  symgfcoeu  33163  symgcom  33164  tocycf  33198  tocyc01  33199  cycpmconjvlem  33222  cycpmconjv  33223  cycpmconjslem1  33235  cycpmconjslem2  33236  cycpmconjs  33237  cyc3conja  33238  1arithidomlem2  33619  selvascl  33701  mplvrpmga  33729  mplvrpmrhm  33731  esplyfval  33747  esplyfval0  33748  esplyfval2  33749  vieta  33764  smatfval  33979  eulerpartlemgv  34557  eulerpartlemn  34565  eulerpart  34566  sseqval  34572  reprpmtf1o  34810  erdsze2lem2  35432  cvmliftlem10  35522  mrsubval  35737  ftc1anclem8  38067  cocnv  38092  ltrncoidN  40620  trlcoabs2N  41214  cdlemg47a  41226  cdlemg46  41227  cdlemg47  41228  ltrnco4  41231  tendovalco  41257  tendoplcbv  41267  tendopl  41268  tendoplass  41275  cdlemi2  41311  cdlemk2  41324  cdlemk4  41326  cdlemk8  41330  cdlemkuu  41387  cdlemk53  41449  cdlemk54  41450  cdlemk55a  41451  erngdvlem3  41482  erngdvlem3-rN  41490  tendocnv  41513  tendospcanN  41515  dvhvaddcbv  41581  dvhvaddval  41582  dvhvaddass  41589  dvhvscacbv  41590  dvhvscaval  41591  dvhopvsca  41594  dvhlveclem  41600  dvhopspN  41607  diblss  41662  cdlemn8  41696  dihopelvalcpre  41740  dihmeetlem1N  41782  dihglblem5apreN  41783  dih1dimatlem0  41820  dihjatcclem4  41913  aks6d1c6lem5  42662  mhmcoaddpsr  43031  rhmcomulpsr  43032  rhmpsr  43033  diophrw  43208  eldioph2  43211  relexpaddss  44162  trclfvcom  44167  frege131d  44208  fsovrfovd  44453  hoicvrrex  46999  ovnlecvr  47001  ovncvrrp  47007  ovn0lem  47008  ovnsubaddlem1  47013  ovnsubadd  47015  ovnhoilem1  47044  ovnhoi  47046  ovnlecvr2  47053  ovncvr2  47054  hspmbl  47072  ovnovollem1  47099  ovnovollem3  47101  3f1oss2  47539  cosn  49324  fuco11id  49824  fucoid  49838  precofval3  49861  prcofvalg  49866  prcofval  49868