Theorem coeq2d 5819

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-br 5101  df-opab 5163  df-co 5641

This theorem is referenced by:  coeq12d  5821  dfpo2  6262  f1ococnv1  6811  funcoeqres  6813  fcof1oinvd  7249  foeqcnvco  7256  f1ofvswap  7262  coof  7656  fparlem3  8066  fparlem4  8067  offsplitfpar  8071  csbwrecsg  8270  mapen  9081  mapfien  9323  wemapwe  9618  hashfacen  14389  s1co  14768  pfxco  14773  relexpsucnnl  14965  relexpsucl  14966  relexpsucld  14969  relexpcnv  14970  relexpaddnn  14986  relexpaddg  14988  prdsval  17387  isofval  17693  cofuass  17825  cofurid  17827  fucid  17910  setcinv  18026  catcisolem  18046  curf2ndf  18182  pwsco2mhm  18770  symggrplem  18821  smndex1igid  18841  f1omvdco2  19389  psgnunilem1  19434  efginvrel2  19668  efginvrel1  19669  vrgpinv  19710  frgpuplem  19713  gsumval3  19848  gsumzf1o  19853  psrass1lem  21900  mpfrcl  22052  evlsval  22053  selvval  22090  evls1fval  22275  evl1fval  22284  pf1mpf  22308  pf1ind  22311  mhmcoaddmpl  22337  rhmcomulmpl  22338  rhmmpl  22339  rhmply1vr1  22343  rhmply1vsca  22344  ofco2  22407  qtophmeo  23773  ustssco  24171  utop2nei  24206  neipcfilu  24251  tngds  24604  elovolmr  25445  ovoliunlem3  25473  uniioombllem2  25552  hoddi  32078  fcoinver  32691  fmptco1f1o  32723  fcobij  32810  cocnvf1o  32819  symgfcoeu  33176  symgcom  33177  tocycf  33211  tocyc01  33212  cycpmconjvlem  33235  cycpmconjv  33236  cycpmconjslem1  33248  cycpmconjslem2  33249  cycpmconjs  33250  cyc3conja  33251  1arithidomlem2  33629  mplvrpmga  33722  mplvrpmrhm  33724  esplyfval  33740  esplyfval0  33741  esplyfval2  33742  vieta  33757  smatfval  33973  eulerpartlemgv  34551  eulerpartlemn  34559  eulerpart  34560  sseqval  34566  reprpmtf1o  34804  erdsze2lem2  35420  cvmliftlem10  35510  mrsubval  35725  ftc1anclem8  37951  cocnv  37976  ltrncoidN  40504  trlcoabs2N  41098  cdlemg47a  41110  cdlemg46  41111  cdlemg47  41112  ltrnco4  41115  tendovalco  41141  tendoplcbv  41151  tendopl  41152  tendoplass  41159  cdlemi2  41195  cdlemk2  41208  cdlemk4  41210  cdlemk8  41214  cdlemkuu  41271  cdlemk53  41333  cdlemk54  41334  cdlemk55a  41335  erngdvlem3  41366  erngdvlem3-rN  41374  tendocnv  41397  tendospcanN  41399  dvhvaddcbv  41465  dvhvaddval  41466  dvhvaddass  41473  dvhvscacbv  41474  dvhvscaval  41475  dvhopvsca  41478  dvhlveclem  41484  dvhopspN  41491  diblss  41546  cdlemn8  41580  dihopelvalcpre  41624  dihmeetlem1N  41666  dihglblem5apreN  41667  dih1dimatlem0  41704  dihjatcclem4  41797  aks6d1c6lem5  42547  mhmcoaddpsr  42918  rhmcomulpsr  42919  rhmpsr  42920  diophrw  43116  eldioph2  43119  relexpaddss  44074  trclfvcom  44079  frege131d  44120  fsovrfovd  44365  hoicvrrex  46914  ovnlecvr  46916  ovncvrrp  46922  ovn0lem  46923  ovnsubaddlem1  46928  ovnsubadd  46930  ovnhoilem1  46959  ovnhoi  46961  ovnlecvr2  46968  ovncvr2  46969  hspmbl  46987  ovnovollem1  47014  ovnovollem3  47016  3f1oss2  47436  cosn  49193  fuco11id  49693  fucoid  49707  precofval3  49730  prcofvalg  49735  prcofval  49737