Theorem coeq2d 5816

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-br 5103  df-opab 5165  df-co 5640

This theorem is referenced by:  coeq12d  5818  dfpo2  6257  f1ococnv1  6811  funcoeqres  6813  fcof1oinvd  7250  foeqcnvco  7257  f1ofvswap  7263  coof  7657  fparlem3  8070  fparlem4  8071  offsplitfpar  8075  csbwrecsg  8274  mapen  9082  mapfien  9335  wemapwe  9626  hashfacen  14395  s1co  14775  pfxco  14780  relexpsucnnl  14972  relexpsucl  14973  relexpsucld  14976  relexpcnv  14977  relexpaddnn  14993  relexpaddg  14995  prdsval  17394  isofval  17695  cofuass  17827  cofurid  17829  fucid  17912  setcinv  18028  catcisolem  18048  curf2ndf  18184  pwsco2mhm  18736  symggrplem  18787  smndex1igid  18807  f1omvdco2  19354  psgnunilem1  19399  efginvrel2  19633  efginvrel1  19634  vrgpinv  19675  frgpuplem  19678  gsumval3  19813  gsumzf1o  19818  psrass1lem  21817  mpfrcl  21968  evlsval  21969  selvval  21998  evls1fval  22182  evl1fval  22191  pf1mpf  22215  pf1ind  22218  mhmcoaddmpl  22244  rhmcomulmpl  22245  rhmmpl  22246  rhmply1vr1  22250  rhmply1vsca  22251  ofco2  22314  qtophmeo  23680  ustssco  24078  utop2nei  24114  neipcfilu  24159  tngds  24512  elovolmr  25353  ovoliunlem3  25381  uniioombllem2  25460  hoddi  31892  fcoinver  32506  fmptco1f1o  32530  fcobij  32618  symgfcoeu  33012  symgcom  33013  tocycf  33047  tocyc01  33048  cycpmconjvlem  33071  cycpmconjv  33072  cycpmconjslem1  33084  cycpmconjslem2  33085  cycpmconjs  33086  cyc3conja  33087  1arithidomlem2  33480  smatfval  33758  eulerpartlemgv  34337  eulerpartlemn  34345  eulerpart  34346  sseqval  34352  reprpmtf1o  34590  erdsze2lem2  35164  cvmliftlem10  35254  mrsubval  35469  ftc1anclem8  37667  cocnv  37692  ltrncoidN  40095  trlcoabs2N  40689  cdlemg47a  40701  cdlemg46  40702  cdlemg47  40703  ltrnco4  40706  tendovalco  40732  tendoplcbv  40742  tendopl  40743  tendoplass  40750  cdlemi2  40786  cdlemk2  40799  cdlemk4  40801  cdlemk8  40805  cdlemkuu  40862  cdlemk53  40924  cdlemk54  40925  cdlemk55a  40926  erngdvlem3  40957  erngdvlem3-rN  40965  tendocnv  40988  tendospcanN  40990  dvhvaddcbv  41056  dvhvaddval  41057  dvhvaddass  41064  dvhvscacbv  41065  dvhvscaval  41066  dvhopvsca  41069  dvhlveclem  41075  dvhopspN  41082  diblss  41137  cdlemn8  41171  dihopelvalcpre  41215  dihmeetlem1N  41257  dihglblem5apreN  41258  dih1dimatlem0  41295  dihjatcclem4  41388  aks6d1c6lem5  42138  mhmcoaddpsr  42511  rhmcomulpsr  42512  rhmpsr  42513  diophrw  42720  eldioph2  42723  relexpaddss  43680  trclfvcom  43685  frege131d  43726  fsovrfovd  43971  hoicvrrex  46527  ovnlecvr  46529  ovncvrrp  46535  ovn0lem  46536  ovnsubaddlem1  46541  ovnsubadd  46543  ovnhoilem1  46572  ovnhoi  46574  ovnlecvr2  46581  ovncvr2  46582  hspmbl  46600  ovnovollem1  46627  ovnovollem3  46629  3f1oss2  47050  cosn  48795  fuco11id  49296  fucoid  49310  precofval3  49333  prcofvalg  49338  prcofval  49340