Theorem coeq2d 5860

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-br 5148  df-opab 5210  df-co 5684

This theorem is referenced by:  coeq12d  5862  dfpo2  6292  f1ococnv1  6859  funcoeqres  6861  fcof1oinvd  7287  foeqcnvco  7294  f1ofvswap  7300  fparlem3  8096  fparlem4  8097  offsplitfpar  8101  csbwrecsg  8302  mapen  9137  mapfien  9399  wemapwe  9688  hashfacen  14409  hashfacenOLD  14410  s1co  14780  pfxco  14785  relexpsucnnl  14973  relexpsucl  14974  relexpsucld  14977  relexpcnv  14978  relexpaddnn  14994  relexpaddg  14996  prdsval  17397  isofval  17700  cofuass  17835  cofurid  17837  fucid  17920  setcinv  18036  catcisolem  18056  curf2ndf  18196  pwsco2mhm  18710  symggrplem  18761  smndex1igid  18781  f1omvdco2  19310  psgnunilem1  19355  efginvrel2  19589  efginvrel1  19590  vrgpinv  19631  frgpuplem  19634  gsumval3  19769  gsumzf1o  19774  psrass1lemOLD  21484  psrass1lem  21487  mpfrcl  21639  evlsval  21640  selvval  21672  evls1fval  21829  evl1fval  21838  pf1mpf  21862  pf1ind  21865  ofco2  21944  qtophmeo  23312  ustssco  23710  utop2nei  23746  neipcfilu  23792  tngds  24155  tngdsOLD  24156  elovolmr  24984  ovoliunlem3  25012  uniioombllem2  25091  hoddi  31230  fcoinver  31822  fmptco1f1o  31844  fcobij  31934  symgfcoeu  32230  symgcom  32231  tocycf  32263  tocyc01  32264  cycpmconjvlem  32287  cycpmconjv  32288  cycpmconjslem1  32300  cycpmconjslem2  32301  cycpmconjs  32302  cyc3conja  32303  smatfval  32763  eulerpartlemgv  33360  eulerpartlemn  33368  eulerpart  33369  sseqval  33375  reprpmtf1o  33626  erdsze2lem2  34183  cvmliftlem10  34273  mrsubval  34488  ftc1anclem8  36556  cocnv  36581  ltrncoidN  38987  trlcoabs2N  39581  cdlemg47a  39593  cdlemg46  39594  cdlemg47  39595  ltrnco4  39598  tendovalco  39624  tendoplcbv  39634  tendopl  39635  tendoplass  39642  cdlemi2  39678  cdlemk2  39691  cdlemk4  39693  cdlemk8  39697  cdlemkuu  39754  cdlemk53  39816  cdlemk54  39817  cdlemk55a  39818  erngdvlem3  39849  erngdvlem3-rN  39857  tendocnv  39880  tendospcanN  39882  dvhvaddcbv  39948  dvhvaddval  39949  dvhvaddass  39956  dvhvscacbv  39957  dvhvscaval  39958  dvhopvsca  39961  dvhlveclem  39967  dvhopspN  39974  diblss  40029  cdlemn8  40063  dihopelvalcpre  40107  dihmeetlem1N  40149  dihglblem5apreN  40150  dih1dimatlem0  40187  dihjatcclem4  40280  mhmcoaddmpl  41120  rhmcomulmpl  41121  rhmmpl  41122  diophrw  41482  eldioph2  41485  relexpaddss  42454  trclfvcom  42459  frege131d  42500  fsovrfovd  42745  hoicvrrex  45258  ovnlecvr  45260  ovncvrrp  45266  ovn0lem  45267  ovnsubaddlem1  45272  ovnsubadd  45274  ovnhoilem1  45303  ovnhoi  45305  ovnlecvr2  45312  ovncvr2  45313  hspmbl  45331  ovnovollem1  45358  ovnovollem3  45360