Theorem coeq2d 5873

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-co 5694

This theorem is referenced by:  coeq12d  5875  dfpo2  6316  f1ococnv1  6877  funcoeqres  6879  fcof1oinvd  7313  foeqcnvco  7320  f1ofvswap  7326  coof  7721  fparlem3  8139  fparlem4  8140  offsplitfpar  8144  csbwrecsg  8346  mapen  9181  mapfien  9448  wemapwe  9737  hashfacen  14493  s1co  14872  pfxco  14877  relexpsucnnl  15069  relexpsucl  15070  relexpsucld  15073  relexpcnv  15074  relexpaddnn  15090  relexpaddg  15092  prdsval  17500  isofval  17801  cofuass  17934  cofurid  17936  fucid  18019  setcinv  18135  catcisolem  18155  curf2ndf  18292  pwsco2mhm  18846  symggrplem  18897  smndex1igid  18917  f1omvdco2  19466  psgnunilem1  19511  efginvrel2  19745  efginvrel1  19746  vrgpinv  19787  frgpuplem  19790  gsumval3  19925  gsumzf1o  19930  psrass1lem  21952  mpfrcl  22109  evlsval  22110  selvval  22139  evls1fval  22323  evl1fval  22332  pf1mpf  22356  pf1ind  22359  mhmcoaddmpl  22385  rhmcomulmpl  22386  rhmmpl  22387  rhmply1vr1  22391  rhmply1vsca  22392  ofco2  22457  qtophmeo  23825  ustssco  24223  utop2nei  24259  neipcfilu  24305  tngds  24668  tngdsOLD  24669  elovolmr  25511  ovoliunlem3  25539  uniioombllem2  25618  hoddi  32009  fcoinver  32617  fmptco1f1o  32643  fcobij  32733  symgfcoeu  33102  symgcom  33103  tocycf  33137  tocyc01  33138  cycpmconjvlem  33161  cycpmconjv  33162  cycpmconjslem1  33174  cycpmconjslem2  33175  cycpmconjs  33176  cyc3conja  33177  1arithidomlem2  33564  smatfval  33794  eulerpartlemgv  34375  eulerpartlemn  34383  eulerpart  34384  sseqval  34390  reprpmtf1o  34641  erdsze2lem2  35209  cvmliftlem10  35299  mrsubval  35514  ftc1anclem8  37707  cocnv  37732  ltrncoidN  40130  trlcoabs2N  40724  cdlemg47a  40736  cdlemg46  40737  cdlemg47  40738  ltrnco4  40741  tendovalco  40767  tendoplcbv  40777  tendopl  40778  tendoplass  40785  cdlemi2  40821  cdlemk2  40834  cdlemk4  40836  cdlemk8  40840  cdlemkuu  40897  cdlemk53  40959  cdlemk54  40960  cdlemk55a  40961  erngdvlem3  40992  erngdvlem3-rN  41000  tendocnv  41023  tendospcanN  41025  dvhvaddcbv  41091  dvhvaddval  41092  dvhvaddass  41099  dvhvscacbv  41100  dvhvscaval  41101  dvhopvsca  41104  dvhlveclem  41110  dvhopspN  41117  diblss  41172  cdlemn8  41206  dihopelvalcpre  41250  dihmeetlem1N  41292  dihglblem5apreN  41293  dih1dimatlem0  41330  dihjatcclem4  41423  aks6d1c6lem5  42178  mhmcoaddpsr  42560  rhmcomulpsr  42561  rhmpsr  42562  diophrw  42770  eldioph2  42773  relexpaddss  43731  trclfvcom  43736  frege131d  43777  fsovrfovd  44022  hoicvrrex  46571  ovnlecvr  46573  ovncvrrp  46579  ovn0lem  46580  ovnsubaddlem1  46585  ovnsubadd  46587  ovnhoilem1  46616  ovnhoi  46618  ovnlecvr2  46625  ovncvr2  46626  hspmbl  46644  ovnovollem1  46671  ovnovollem3  46673  3f1oss2  47088  cosn  48745  fuco11id  49029  fucoid  49043  precoffunc  49066