Theorem coeq2d 5851

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∘ ccom 5668

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ss 3925  df-br 5113  df-opab 5177  df-co 5673

This theorem is used by:  coeq12d  5853  dfpo2  6301  f1ococnv1  6854  funcoeqres  6856  fcof1oinvd  7295  foeqcnvco  7302  f1ofvswap  7308  coof  7704  fparlem3  8111  fparlem4  8112  offsplitfpar  8116  csbwrecsg  8317  mapen  9131  mapfien  9370  wemapwe  9668  hashfacen  14502  s1co  14881  pfxco  14886  relexpsucnnl  15078  relexpsucl  15079  relexpsucld  15082  relexpcnv  15083  relexpaddnn  15099  relexpaddg  15101  prdsval  17518  isofval  17824  cofuass  17956  cofurid  17958  fucid  18041  setcinv  18157  catcisolem  18177  curf2ndf  18313  pwsco2mhm  18902  symggrplem  18953  smndex1igid  18975  smndex1igidOLD  18976  f1omvdco2  19528  psgnunilem1  19573  efginvrel2  19807  efginvrel1  19808  vrgpinv  19849  frgpuplem  19852  gsumval3  19987  gsumzf1o  19992  psrass1lem  22098  mpfrcl  22251  evlsval  22252  selvval  22286  mhmcoaddmpl  22289  rhmcomulmpl  22290  evls1fval  22494  evl1fval  22503  pf1mpf  22527  pf1ind  22530  rhmmpl  22555  rhmply1vr1  22559  rhmply1vsca  22560  ofco2  22623  qtophmeo  23989  ustssco  24387  utop2nei  24422  neipcfilu  24467  tngds  24820  elovolmr  25650  ovoliunlem3  25678  uniioombllem2  25757  hoddi  32357  fcoinver  32964  fmptco1f1o  32993  fcobij  33080  cocnvf1o  33089  symgfcoeu  33415  symgcom  33416  tocycf  33450  tocyc01  33451  cycpmconjvlem  33474  cycpmconjv  33475  cycpmconjslem1  33487  cycpmconjslem2  33488  cycpmconjs  33489  cyc3conja  33490  1arithidomlem2  33839  selvascl  33920  mplvrpmga  33948  mplvrpmrhm  33950  esplyfval  33966  esplyfval0  33967  esplyfval2  33968  vieta  33983  smatfval  34198  eulerpartlemgv  34776  eulerpartlemn  34784  eulerpart  34785  sseqval  34791  reprpmtf1o  35026  erdsze2lem2  35708  cvmliftlem10  35798  mrsubval  36013  ftc1anclem8  38383  cocnv  38408  ltrncoidN  40934  trlcoabs2N  41528  cdlemg47a  41540  cdlemg46  41541  cdlemg47  41542  ltrnco4  41545  tendovalco  41571  tendoplcbv  41581  tendopl  41582  tendoplass  41589  cdlemi2  41625  cdlemk2  41638  cdlemk4  41640  cdlemk8  41644  cdlemkuu  41701  cdlemk53  41763  cdlemk54  41764  cdlemk55a  41765  erngdvlem3  41796  erngdvlem3-rN  41804  tendocnv  41827  tendospcanN  41829  dvhvaddcbv  41895  dvhvaddval  41896  dvhvaddass  41903  dvhvscacbv  41904  dvhvscaval  41905  dvhopvsca  41908  dvhlveclem  41914  dvhopspN  41921  diblss  41976  cdlemn8  42010  dihopelvalcpre  42054  dihmeetlem1N  42096  dihglblem5apreN  42097  dih1dimatlem0  42134  dihjatcclem4  42227  aks6d1c6lem5  42976  mhmcoaddpsr  43345  rhmcomulpsr  43346  rhmpsr  43347  diophrw  43522  eldioph2  43525  relexpaddss  44476  trclfvcom  44481  frege131d  44522  fsovrfovd  44767  hoicvrrex  47302  ovnlecvr  47304  ovncvrrp  47310  ovn0lem  47311  ovnsubaddlem1  47316  ovnsubadd  47318  ovnhoilem1  47347  ovnhoi  47349  ovnlecvr2  47356  ovncvr2  47357  hspmbl  47375  ovnovollem1  47402  ovnovollem3  47404  3f1oss2  47845  cosn  49644  fuco11id  50144  fucoid  50158  precofval3  50181  prcofvalg  50186  prcofval  50188