Theorem coeq2d 5791

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

Syntax hints:   → wi 4   = wceq 1540   ∘ ccom 5611

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-in 3904  df-ss 3914  df-br 5088  df-opab 5150  df-co 5616

This theorem is referenced by:  coeq12d  5793  dfpo2  6221  f1ococnv1  6782  funcoeqres  6784  fcof1oinvd  7204  foeqcnvco  7211  f1ofvswap  7217  fparlem3  7999  fparlem4  8000  offsplitfpar  8004  csbwrecsg  8184  mapen  8983  mapfien  9237  wemapwe  9526  hashfacen  14238  hashfacenOLD  14239  s1co  14618  pfxco  14623  relexpsucnnl  14813  relexpsucl  14814  relexpsucld  14817  relexpcnv  14818  relexpaddnn  14834  relexpaddg  14836  prdsval  17236  isofval  17539  cofuass  17674  cofurid  17676  fucid  17759  setcinv  17875  catcisolem  17895  curf2ndf  18035  pwsco2mhm  18541  symggrplem  18592  smndex1igid  18612  f1omvdco2  19125  psgnunilem1  19170  efginvrel2  19401  efginvrel1  19402  vrgpinv  19443  frgpuplem  19446  gsumval3  19576  gsumzf1o  19581  psrass1lemOLD  21215  psrass1lem  21218  mpfrcl  21367  evlsval  21368  selvval  21400  evls1fval  21557  evl1fval  21566  pf1mpf  21590  pf1ind  21593  ofco2  21672  qtophmeo  23040  ustssco  23438  utop2nei  23474  neipcfilu  23520  tngds  23883  tngdsOLD  23884  elovolmr  24712  ovoliunlem3  24740  uniioombllem2  24819  hoddi  30461  fcoinver  31054  fmptco1f1o  31076  fcobij  31165  symgfcoeu  31459  symgcom  31460  tocycf  31492  tocyc01  31493  cycpmconjvlem  31516  cycpmconjv  31517  cycpmconjslem1  31529  cycpmconjslem2  31530  cycpmconjs  31531  cyc3conja  31532  smatfval  31851  eulerpartlemgv  32446  eulerpartlemn  32454  eulerpart  32455  sseqval  32461  reprpmtf1o  32712  erdsze2lem2  33271  cvmliftlem10  33361  mrsubval  33576  ftc1anclem8  35913  cocnv  35939  ltrncoidN  38347  trlcoabs2N  38941  cdlemg47a  38953  cdlemg46  38954  cdlemg47  38955  ltrnco4  38958  tendovalco  38984  tendoplcbv  38994  tendopl  38995  tendoplass  39002  cdlemi2  39038  cdlemk2  39051  cdlemk4  39053  cdlemk8  39057  cdlemkuu  39114  cdlemk53  39176  cdlemk54  39177  cdlemk55a  39178  erngdvlem3  39209  erngdvlem3-rN  39217  tendocnv  39240  tendospcanN  39242  dvhvaddcbv  39308  dvhvaddval  39309  dvhvaddass  39316  dvhvscacbv  39317  dvhvscaval  39318  dvhopvsca  39321  dvhlveclem  39327  dvhopspN  39334  diblss  39389  cdlemn8  39423  dihopelvalcpre  39467  dihmeetlem1N  39509  dihglblem5apreN  39510  dih1dimatlem0  39547  dihjatcclem4  39640  diophrw  40784  eldioph2  40787  relexpaddss  41547  trclfvcom  41552  frege131d  41593  fsovrfovd  41838  hoicvrrex  44332  ovnlecvr  44334  ovncvrrp  44340  ovn0lem  44341  ovnsubaddlem1  44346  ovnsubadd  44348  ovnhoilem1  44377  ovnhoi  44379  ovnlecvr2  44386  ovncvr2  44387  hspmbl  44405  ovnovollem1  44432  ovnovollem3  44434