Theorem coeq2d 5284

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

Syntax hints:   → wi 4   = wceq 1483   ∘ ccom 5118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-br 4654  df-opab 4713  df-co 5123

This theorem is referenced by:  coeq12d  5286  f1ococnv1  6165  funcoeqres  6167  fcof1oinvd  6548  foeqcnvco  6555  fparlem3  7279  fparlem4  7280  mapen  8124  mapfien  8313  wemapwe  8594  hashfacen  13238  s1co  13579  relexpsucnnl  13772  relexpsucl  13773  relexpcnv  13775  relexpaddnn  13791  relexpaddg  13793  prdsval  16115  isofval  16417  cofuass  16549  cofurid  16551  fucid  16631  setcinv  16740  catcisolem  16756  curf2ndf  16887  pwsco2mhm  17371  symggrp  17820  f1omvdco2  17868  psgnunilem1  17913  efginvrel2  18140  efginvrel1  18141  vrgpinv  18182  frgpuplem  18185  gsumval3  18308  gsumzf1o  18313  psrass1lem  19377  mpfrcl  19518  evlsval  19519  evls1fval  19684  evl1fval  19692  pf1mpf  19716  pf1ind  19719  ofco2  20257  qtophmeo  21620  ustssco  22018  utop2nei  22054  neipcfilu  22100  tngds  22452  elovolmr  23244  ovoliunlem3  23272  uniioombllem2  23351  hoddi  28849  fcoinver  29418  fmptco1f1o  29434  fcobij  29500  symgfcoeu  29845  smatfval  29861  eulerpartlemgv  30435  eulerpartlemn  30443  eulerpart  30444  sseqval  30450  reprpmtf1o  30704  erdsze2lem2  31186  cvmliftlem10  31276  mrsubval  31406  dfpo2  31645  ftc1anclem8  33492  cocnv  33520  ltrncoidN  35414  trlcoabs2N  36010  cdlemg47a  36022  cdlemg46  36023  cdlemg47  36024  ltrnco4  36027  tendovalco  36053  tendoplcbv  36063  tendopl  36064  tendoplass  36071  cdlemi2  36107  cdlemk2  36120  cdlemk4  36122  cdlemk8  36126  cdlemkuu  36183  cdlemk53  36245  cdlemk54  36246  cdlemk55a  36247  erngdvlem3  36278  erngdvlem3-rN  36286  tendocnv  36310  tendospcanN  36312  dvhvaddcbv  36378  dvhvaddval  36379  dvhvaddass  36386  dvhvscacbv  36387  dvhvscaval  36388  dvhopvsca  36391  dvhlveclem  36397  dvhopspN  36404  diblss  36459  cdlemn8  36493  dihopelvalcpre  36537  dihmeetlem1N  36579  dihglblem5apreN  36580  dih1dimatlem0  36617  dihjatcclem4  36710  diophrw  37322  eldioph2  37325  relexpaddss  38010  trclfvcom  38015  frege131d  38056  fsovrfovd  38303  hoicvrrex  40770  ovnlecvr  40772  ovncvrrp  40778  ovn0lem  40779  ovnsubaddlem1  40784  ovnsubadd  40786  ovnhoilem1  40815  ovnhoi  40817  ovnlecvr2  40824  ovncvr2  40825  hspmbl  40843  ovnovollem1  40870  ovnovollem3  40872  pfxco  41438