Theorem coeq2d 5861

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

Syntax hints:   → wi 4   = wceq 1539   ∘ ccom 5679

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-br 5148  df-opab 5210  df-co 5684

This theorem is referenced by:  coeq12d  5863  dfpo2  6294  f1ococnv1  6861  funcoeqres  6863  fcof1oinvd  7293  foeqcnvco  7300  f1ofvswap  7306  fparlem3  8102  fparlem4  8103  offsplitfpar  8107  csbwrecsg  8308  mapen  9143  mapfien  9405  wemapwe  9694  hashfacen  14417  hashfacenOLD  14418  s1co  14788  pfxco  14793  relexpsucnnl  14981  relexpsucl  14982  relexpsucld  14985  relexpcnv  14986  relexpaddnn  15002  relexpaddg  15004  prdsval  17405  isofval  17708  cofuass  17843  cofurid  17845  fucid  17928  setcinv  18044  catcisolem  18064  curf2ndf  18204  pwsco2mhm  18750  symggrplem  18801  smndex1igid  18821  f1omvdco2  19357  psgnunilem1  19402  efginvrel2  19636  efginvrel1  19637  vrgpinv  19678  frgpuplem  19681  gsumval3  19816  gsumzf1o  19821  psrass1lemOLD  21712  psrass1lem  21715  mpfrcl  21867  evlsval  21868  selvval  21900  evls1fval  22058  evl1fval  22067  pf1mpf  22091  pf1ind  22094  ofco2  22173  qtophmeo  23541  ustssco  23939  utop2nei  23975  neipcfilu  24021  tngds  24384  tngdsOLD  24385  elovolmr  25225  ovoliunlem3  25253  uniioombllem2  25332  hoddi  31510  fcoinver  32102  fmptco1f1o  32124  fcobij  32214  symgfcoeu  32513  symgcom  32514  tocycf  32546  tocyc01  32547  cycpmconjvlem  32570  cycpmconjv  32571  cycpmconjslem1  32583  cycpmconjslem2  32584  cycpmconjs  32585  cyc3conja  32586  smatfval  33073  eulerpartlemgv  33670  eulerpartlemn  33678  eulerpart  33679  sseqval  33685  reprpmtf1o  33936  erdsze2lem2  34493  cvmliftlem10  34583  mrsubval  34798  ftc1anclem8  36871  cocnv  36896  ltrncoidN  39302  trlcoabs2N  39896  cdlemg47a  39908  cdlemg46  39909  cdlemg47  39910  ltrnco4  39913  tendovalco  39939  tendoplcbv  39949  tendopl  39950  tendoplass  39957  cdlemi2  39993  cdlemk2  40006  cdlemk4  40008  cdlemk8  40012  cdlemkuu  40069  cdlemk53  40131  cdlemk54  40132  cdlemk55a  40133  erngdvlem3  40164  erngdvlem3-rN  40172  tendocnv  40195  tendospcanN  40197  dvhvaddcbv  40263  dvhvaddval  40264  dvhvaddass  40271  dvhvscacbv  40272  dvhvscaval  40273  dvhopvsca  40276  dvhlveclem  40282  dvhopspN  40289  diblss  40344  cdlemn8  40378  dihopelvalcpre  40422  dihmeetlem1N  40464  dihglblem5apreN  40465  dih1dimatlem0  40502  dihjatcclem4  40595  mhmcoaddmpl  41425  rhmcomulmpl  41426  rhmmpl  41427  diophrw  41799  eldioph2  41802  relexpaddss  42771  trclfvcom  42776  frege131d  42817  fsovrfovd  43062  hoicvrrex  45570  ovnlecvr  45572  ovncvrrp  45578  ovn0lem  45579  ovnsubaddlem1  45584  ovnsubadd  45586  ovnhoilem1  45615  ovnhoi  45617  ovnlecvr2  45624  ovncvr2  45625  hspmbl  45643  ovnovollem1  45670  ovnovollem3  45672