Theorem coeq2d 5829

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

Syntax hints:   → wi 4   = wceq 1540   ∘ ccom 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-co 5650

This theorem is referenced by:  coeq12d  5831  dfpo2  6272  f1ococnv1  6832  funcoeqres  6834  fcof1oinvd  7271  foeqcnvco  7278  f1ofvswap  7284  coof  7680  fparlem3  8096  fparlem4  8097  offsplitfpar  8101  csbwrecsg  8300  mapen  9111  mapfien  9366  wemapwe  9657  hashfacen  14426  s1co  14806  pfxco  14811  relexpsucnnl  15003  relexpsucl  15004  relexpsucld  15007  relexpcnv  15008  relexpaddnn  15024  relexpaddg  15026  prdsval  17425  isofval  17726  cofuass  17858  cofurid  17860  fucid  17943  setcinv  18059  catcisolem  18079  curf2ndf  18215  pwsco2mhm  18767  symggrplem  18818  smndex1igid  18838  f1omvdco2  19385  psgnunilem1  19430  efginvrel2  19664  efginvrel1  19665  vrgpinv  19706  frgpuplem  19709  gsumval3  19844  gsumzf1o  19849  psrass1lem  21848  mpfrcl  21999  evlsval  22000  selvval  22029  evls1fval  22213  evl1fval  22222  pf1mpf  22246  pf1ind  22249  mhmcoaddmpl  22275  rhmcomulmpl  22276  rhmmpl  22277  rhmply1vr1  22281  rhmply1vsca  22282  ofco2  22345  qtophmeo  23711  ustssco  24109  utop2nei  24145  neipcfilu  24190  tngds  24543  elovolmr  25384  ovoliunlem3  25412  uniioombllem2  25491  hoddi  31926  fcoinver  32540  fmptco1f1o  32564  fcobij  32652  symgfcoeu  33046  symgcom  33047  tocycf  33081  tocyc01  33082  cycpmconjvlem  33105  cycpmconjv  33106  cycpmconjslem1  33118  cycpmconjslem2  33119  cycpmconjs  33120  cyc3conja  33121  1arithidomlem2  33514  smatfval  33792  eulerpartlemgv  34371  eulerpartlemn  34379  eulerpart  34380  sseqval  34386  reprpmtf1o  34624  erdsze2lem2  35198  cvmliftlem10  35288  mrsubval  35503  ftc1anclem8  37701  cocnv  37726  ltrncoidN  40129  trlcoabs2N  40723  cdlemg47a  40735  cdlemg46  40736  cdlemg47  40737  ltrnco4  40740  tendovalco  40766  tendoplcbv  40776  tendopl  40777  tendoplass  40784  cdlemi2  40820  cdlemk2  40833  cdlemk4  40835  cdlemk8  40839  cdlemkuu  40896  cdlemk53  40958  cdlemk54  40959  cdlemk55a  40960  erngdvlem3  40991  erngdvlem3-rN  40999  tendocnv  41022  tendospcanN  41024  dvhvaddcbv  41090  dvhvaddval  41091  dvhvaddass  41098  dvhvscacbv  41099  dvhvscaval  41100  dvhopvsca  41103  dvhlveclem  41109  dvhopspN  41116  diblss  41171  cdlemn8  41205  dihopelvalcpre  41249  dihmeetlem1N  41291  dihglblem5apreN  41292  dih1dimatlem0  41329  dihjatcclem4  41422  aks6d1c6lem5  42172  mhmcoaddpsr  42545  rhmcomulpsr  42546  rhmpsr  42547  diophrw  42754  eldioph2  42757  relexpaddss  43714  trclfvcom  43719  frege131d  43760  fsovrfovd  44005  hoicvrrex  46561  ovnlecvr  46563  ovncvrrp  46569  ovn0lem  46570  ovnsubaddlem1  46575  ovnsubadd  46577  ovnhoilem1  46606  ovnhoi  46608  ovnlecvr2  46615  ovncvr2  46616  hspmbl  46634  ovnovollem1  46661  ovnovollem3  46663  3f1oss2  47081  cosn  48826  fuco11id  49327  fucoid  49341  precofval3  49364  prcofvalg  49369  prcofval  49371