Theorem coeq2d 5875

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

Syntax hints:   → wi 4   = wceq 1536   ∘ ccom 5692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ss 3979  df-br 5148  df-opab 5210  df-co 5697

This theorem is referenced by:  coeq12d  5877  dfpo2  6317  f1ococnv1  6877  funcoeqres  6879  fcof1oinvd  7312  foeqcnvco  7319  f1ofvswap  7325  coof  7720  fparlem3  8137  fparlem4  8138  offsplitfpar  8142  csbwrecsg  8344  mapen  9179  mapfien  9445  wemapwe  9734  hashfacen  14489  s1co  14868  pfxco  14873  relexpsucnnl  15065  relexpsucl  15066  relexpsucld  15069  relexpcnv  15070  relexpaddnn  15086  relexpaddg  15088  prdsval  17501  isofval  17804  cofuass  17939  cofurid  17941  fucid  18027  setcinv  18143  catcisolem  18163  curf2ndf  18303  pwsco2mhm  18858  symggrplem  18909  smndex1igid  18929  f1omvdco2  19480  psgnunilem1  19525  efginvrel2  19759  efginvrel1  19760  vrgpinv  19801  frgpuplem  19804  gsumval3  19939  gsumzf1o  19944  psrass1lem  21969  mpfrcl  22126  evlsval  22127  selvval  22156  evls1fval  22338  evl1fval  22347  pf1mpf  22371  pf1ind  22374  mhmcoaddmpl  22400  rhmcomulmpl  22401  rhmmpl  22402  rhmply1vr1  22406  rhmply1vsca  22407  ofco2  22472  qtophmeo  23840  ustssco  24238  utop2nei  24274  neipcfilu  24320  tngds  24683  tngdsOLD  24684  elovolmr  25524  ovoliunlem3  25552  uniioombllem2  25631  hoddi  32018  fcoinver  32623  fmptco1f1o  32649  fcobij  32739  symgfcoeu  33084  symgcom  33085  tocycf  33119  tocyc01  33120  cycpmconjvlem  33143  cycpmconjv  33144  cycpmconjslem1  33156  cycpmconjslem2  33157  cycpmconjs  33158  cyc3conja  33159  1arithidomlem2  33543  smatfval  33755  eulerpartlemgv  34354  eulerpartlemn  34362  eulerpart  34363  sseqval  34369  reprpmtf1o  34619  erdsze2lem2  35188  cvmliftlem10  35278  mrsubval  35493  ftc1anclem8  37686  cocnv  37711  ltrncoidN  40110  trlcoabs2N  40704  cdlemg47a  40716  cdlemg46  40717  cdlemg47  40718  ltrnco4  40721  tendovalco  40747  tendoplcbv  40757  tendopl  40758  tendoplass  40765  cdlemi2  40801  cdlemk2  40814  cdlemk4  40816  cdlemk8  40820  cdlemkuu  40877  cdlemk53  40939  cdlemk54  40940  cdlemk55a  40941  erngdvlem3  40972  erngdvlem3-rN  40980  tendocnv  41003  tendospcanN  41005  dvhvaddcbv  41071  dvhvaddval  41072  dvhvaddass  41079  dvhvscacbv  41080  dvhvscaval  41081  dvhopvsca  41084  dvhlveclem  41090  dvhopspN  41097  diblss  41152  cdlemn8  41186  dihopelvalcpre  41230  dihmeetlem1N  41272  dihglblem5apreN  41273  dih1dimatlem0  41310  dihjatcclem4  41403  aks6d1c6lem5  42158  mhmcoaddpsr  42536  rhmcomulpsr  42537  rhmpsr  42538  diophrw  42746  eldioph2  42749  relexpaddss  43707  trclfvcom  43712  frege131d  43753  fsovrfovd  43998  hoicvrrex  46511  ovnlecvr  46513  ovncvrrp  46519  ovn0lem  46520  ovnsubaddlem1  46525  ovnsubadd  46527  ovnhoilem1  46556  ovnhoi  46558  ovnlecvr2  46565  ovncvr2  46566  hspmbl  46584  ovnovollem1  46611  ovnovollem3  46613  3f1oss2  47025