Theorem coeq2d 4988

Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)

Hypothesis

Ref	Expression
coeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
coeq2d	|- ( ph -> ( C o. A ) = ( C o. B ) )

Proof of Theorem coeq2d

Step	Hyp	Ref	Expression
1		coeq1d.1	. 2 |- ( ph -> A = B )
2		coeq2 4984	. 2 |- ( A = B -> ( C o. A ) = ( C o. B ) )
3	1, 2	syl 17	1 |- ( ph -> ( C o. A ) = ( C o. B ) )

Syntax hints:   -> wi 4   = wceq 1407   o. ccom 4829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-in 3423  df-ss 3430  df-br 4398  df-opab 4456  df-co 4834

This theorem is referenced by:  coeq12d  4990  relcoi1OLD  5355  f1ococnv1  5829  funcoeqres  5831  fcof1oinvd  6181  foeqcnvco  6188  fparlem3  6888  fparlem4  6889  mapen  7721  mapfien  7903  mapfienOLD  8172  wemapwe  8173  wemapweOLD  8174  hashfacen  12554  s1co  12857  relexpsucnnl  13016  relexpsucl  13017  relexpcnv  13019  relexpaddnn  13035  relexpaddg  13037  prdsval  15071  isofval  15372  cofuass  15504  cofurid  15506  fucid  15586  setcinv  15695  catcisolem  15711  curf2ndf  15842  pwsco2mhm  16328  symggrp  16751  f1omvdco2  16799  psgnunilem1  16844  efginvrel2  17071  efginvrel1  17072  vrgpinv  17113  frgpuplem  17116  gsumval3OLD  17234  gsumval3  17237  gsumzf1o  17243  gsumzf1oOLD  17246  psrass1lem  18351  mpfrcl  18509  evlsval  18510  evls1fval  18678  evl1fval  18686  pf1mpf  18710  pf1ind  18713  ofco2  19247  qtophmeo  20612  ustssco  21011  utop2nei  21047  neipcfilu  21093  tngds  21456  elovolmr  22181  ovoliunlem3  22209  uniioombllem2  22286  hoddi  27335  fcoinver  27909  fcobij  28008  eulerpartlemgv  28831  eulerpartlemn  28839  eulerpart  28840  sseqval  28846  erdsze2lem2  29514  cvmliftlem10  29604  mrsubval  29734  dfpo2  29981  ftc1anclem8  31483  cocnv  31511  ltrncoidN  33158  trlcoabs2N  33754  cdlemg47a  33766  cdlemg46  33767  cdlemg47  33768  ltrnco4  33771  tendovalco  33797  tendoplcbv  33807  tendopl  33808  tendoplass  33815  cdlemi2  33851  cdlemk2  33864  cdlemk4  33866  cdlemk8  33870  cdlemkuu  33927  cdlemk53  33989  cdlemk54  33990  cdlemk55a  33991  erngdvlem3  34022  erngdvlem3-rN  34030  tendocnv  34054  tendospcanN  34056  dvhvaddcbv  34122  dvhvaddval  34123  dvhvaddass  34130  dvhvscacbv  34131  dvhvscaval  34132  dvhopvsca  34135  dvhlveclem  34141  dvhopspN  34148  diblss  34203  cdlemn8  34237  dihopelvalcpre  34281  dihmeetlem1N  34323  dihglblem5apreN  34324  dih1dimatlem0  34361  dihjatcclem4  34454  diophrw  35066  eldioph2  35069  relexpaddss  35710  trclfvcom  35715  frege131d  35756  pfxco  37938