Theorem coeq2d 5733

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

Syntax hints:   → wi 4   = wceq 1537   ∘ ccom 5559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3943  df-ss 3952  df-br 5067  df-opab 5129  df-co 5564

This theorem is referenced by:  coeq12d  5735  f1ococnv1  6643  funcoeqres  6645  fcof1oinvd  7049  foeqcnvco  7056  fparlem3  7809  fparlem4  7810  offsplitfpar  7815  mapen  8681  mapfien  8871  wemapwe  9160  hashfacen  13813  s1co  14195  pfxco  14200  relexpsucnnl  14391  relexpsucl  14392  relexpcnv  14394  relexpaddnn  14410  relexpaddg  14412  prdsval  16728  isofval  17027  cofuass  17159  cofurid  17161  fucid  17241  setcinv  17350  catcisolem  17366  curf2ndf  17497  pwsco2mhm  17997  symggrplem  18049  smndex1igid  18069  f1omvdco2  18576  psgnunilem1  18621  efginvrel2  18853  efginvrel1  18854  vrgpinv  18895  frgpuplem  18898  gsumval3  19027  gsumzf1o  19032  psrass1lem  20157  mpfrcl  20298  evlsval  20299  selvval  20331  evls1fval  20482  evl1fval  20491  pf1mpf  20515  pf1ind  20518  ofco2  21060  qtophmeo  22425  ustssco  22823  utop2nei  22859  neipcfilu  22905  tngds  23257  elovolmr  24077  ovoliunlem3  24105  uniioombllem2  24184  hoddi  29767  fcoinver  30357  fmptco1f1o  30378  fcobij  30458  symgfcoeu  30726  symgcom  30727  tocycf  30759  tocyc01  30760  cycpmconjvlem  30783  cycpmconjv  30784  cycpmconjslem1  30796  cycpmconjslem2  30797  cycpmconjs  30798  cyc3conja  30799  smatfval  31060  eulerpartlemgv  31631  eulerpartlemn  31639  eulerpart  31640  sseqval  31646  reprpmtf1o  31897  erdsze2lem2  32451  cvmliftlem10  32541  mrsubval  32756  dfpo2  32991  ftc1anclem8  34989  cocnv  35015  ltrncoidN  37279  trlcoabs2N  37873  cdlemg47a  37885  cdlemg46  37886  cdlemg47  37887  ltrnco4  37890  tendovalco  37916  tendoplcbv  37926  tendopl  37927  tendoplass  37934  cdlemi2  37970  cdlemk2  37983  cdlemk4  37985  cdlemk8  37989  cdlemkuu  38046  cdlemk53  38108  cdlemk54  38109  cdlemk55a  38110  erngdvlem3  38141  erngdvlem3-rN  38149  tendocnv  38172  tendospcanN  38174  dvhvaddcbv  38240  dvhvaddval  38241  dvhvaddass  38248  dvhvscacbv  38249  dvhvscaval  38250  dvhopvsca  38253  dvhlveclem  38259  dvhopspN  38266  diblss  38321  cdlemn8  38355  dihopelvalcpre  38399  dihmeetlem1N  38441  dihglblem5apreN  38442  dih1dimatlem0  38479  dihjatcclem4  38572  diophrw  39376  eldioph2  39379  relexpaddss  40083  trclfvcom  40088  frege131d  40129  fsovrfovd  40375  hoicvrrex  42858  ovnlecvr  42860  ovncvrrp  42866  ovn0lem  42867  ovnsubaddlem1  42872  ovnsubadd  42874  ovnhoilem1  42903  ovnhoi  42905  ovnlecvr2  42912  ovncvr2  42913  hspmbl  42931  ovnovollem1  42958  ovnovollem3  42960