Theorem coeq2d 5817

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

Syntax hints:   → wi 4   = wceq 1542   ∘ ccom 5635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-br 5086  df-opab 5148  df-co 5640

This theorem is referenced by:  coeq12d  5819  dfpo2  6260  f1ococnv1  6809  funcoeqres  6811  fcof1oinvd  7248  foeqcnvco  7255  f1ofvswap  7261  coof  7655  fparlem3  8064  fparlem4  8065  offsplitfpar  8069  csbwrecsg  8268  mapen  9079  mapfien  9321  wemapwe  9618  hashfacen  14416  s1co  14795  pfxco  14800  relexpsucnnl  14992  relexpsucl  14993  relexpsucld  14996  relexpcnv  14997  relexpaddnn  15013  relexpaddg  15015  prdsval  17418  isofval  17724  cofuass  17856  cofurid  17858  fucid  17941  setcinv  18057  catcisolem  18077  curf2ndf  18213  pwsco2mhm  18801  symggrplem  18852  smndex1igid  18874  smndex1igidOLD  18875  f1omvdco2  19423  psgnunilem1  19468  efginvrel2  19702  efginvrel1  19703  vrgpinv  19744  frgpuplem  19747  gsumval3  19882  gsumzf1o  19887  psrass1lem  21912  mpfrcl  22063  evlsval  22064  selvval  22101  evls1fval  22284  evl1fval  22293  pf1mpf  22317  pf1ind  22320  mhmcoaddmpl  22346  rhmcomulmpl  22347  rhmmpl  22348  rhmply1vr1  22352  rhmply1vsca  22353  ofco2  22416  qtophmeo  23782  ustssco  24180  utop2nei  24215  neipcfilu  24260  tngds  24613  elovolmr  25443  ovoliunlem3  25471  uniioombllem2  25550  hoddi  32061  fcoinver  32674  fmptco1f1o  32706  fcobij  32793  cocnvf1o  32802  symgfcoeu  33143  symgcom  33144  tocycf  33178  tocyc01  33179  cycpmconjvlem  33202  cycpmconjv  33203  cycpmconjslem1  33215  cycpmconjslem2  33216  cycpmconjs  33217  cyc3conja  33218  1arithidomlem2  33596  mplvrpmga  33689  mplvrpmrhm  33691  esplyfval  33707  esplyfval0  33708  esplyfval2  33709  vieta  33724  smatfval  33939  eulerpartlemgv  34517  eulerpartlemn  34525  eulerpart  34526  sseqval  34532  reprpmtf1o  34770  erdsze2lem2  35386  cvmliftlem10  35476  mrsubval  35691  ftc1anclem8  38021  cocnv  38046  ltrncoidN  40574  trlcoabs2N  41168  cdlemg47a  41180  cdlemg46  41181  cdlemg47  41182  ltrnco4  41185  tendovalco  41211  tendoplcbv  41221  tendopl  41222  tendoplass  41229  cdlemi2  41265  cdlemk2  41278  cdlemk4  41280  cdlemk8  41284  cdlemkuu  41341  cdlemk53  41403  cdlemk54  41404  cdlemk55a  41405  erngdvlem3  41436  erngdvlem3-rN  41444  tendocnv  41467  tendospcanN  41469  dvhvaddcbv  41535  dvhvaddval  41536  dvhvaddass  41543  dvhvscacbv  41544  dvhvscaval  41545  dvhopvsca  41548  dvhlveclem  41554  dvhopspN  41561  diblss  41616  cdlemn8  41650  dihopelvalcpre  41694  dihmeetlem1N  41736  dihglblem5apreN  41737  dih1dimatlem0  41774  dihjatcclem4  41867  aks6d1c6lem5  42616  mhmcoaddpsr  42993  rhmcomulpsr  42994  rhmpsr  42995  diophrw  43191  eldioph2  43194  relexpaddss  44145  trclfvcom  44150  frege131d  44191  fsovrfovd  44436  hoicvrrex  46984  ovnlecvr  46986  ovncvrrp  46992  ovn0lem  46993  ovnsubaddlem1  46998  ovnsubadd  47000  ovnhoilem1  47029  ovnhoi  47031  ovnlecvr2  47038  ovncvr2  47039  hspmbl  47057  ovnovollem1  47084  ovnovollem3  47086  3f1oss2  47524  cosn  49309  fuco11id  49809  fucoid  49823  precofval3  49846  prcofvalg  49851  prcofval  49853