Theorem coeq2d 4998

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 4994	. 2 |- ( A = B -> ( C o. A ) = ( C o. B ) )
3	1, 2	syl 16	1 |- ( ph -> ( C o. A ) = ( C o. B ) )

Syntax hints:   -> wi 4   = wceq 1364   o. ccom 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-in 3332  df-ss 3339  df-br 4290  df-opab 4348  df-co 4845

This theorem is referenced by:  coeq12d  5000  relcoi1  5363  f1ococnv1  5666  funcoeqres  5668  fcof1o  5994  foeqcnvco  5995  fparlem3  6673  fparlem4  6674  mapen  7471  mapfien  7653  mapfienOLD  7923  wemapwe  7924  wemapweOLD  7925  hashfacen  12203  s1co  12457  prdsval  14389  isoval  14699  cofuass  14795  cofurid  14797  fucid  14877  setcinv  14954  catcisolem  14970  curf2ndf  15053  pwsco2mhm  15494  symggrp  15898  f1omvdco2  15947  psgnunilem1  15992  efginvrel2  16217  efginvrel1  16218  vrgpinv  16259  frgpuplem  16262  gsumval3OLD  16375  gsumval3  16378  gsumzf1o  16384  gsumzf1oOLD  16387  psrass1lem  17425  mpfrcl  17580  evlsval  17581  evls1fval  17727  evl1fval  17732  pf1mpf  17755  pf1ind  17758  ofco2  18291  qtophmeo  19349  ustssco  19748  utop2nei  19784  neipcfilu  19830  tngds  20193  elovolmr  20918  ovoliunlem3  20946  uniioombllem2  21022  hoddi  25329  fcobij  25960  eulerpartlemgv  26686  eulerpartlemn  26694  eulerpart  26695  sseqval  26701  erdsze2lem2  27022  cvmliftlem10  27113  relexpsucl  27263  relexpadd  27269  dfpo2  27494  ftc1anclem8  28399  cocnv  28544  diophrw  29022  eldioph2  29025  ltrncoidN  33494  trlcoabs2N  34088  cdlemg47a  34100  cdlemg46  34101  cdlemg47  34102  ltrnco4  34105  tendovalco  34131  tendoplcbv  34141  tendopl  34142  tendoplass  34149  cdlemi2  34185  cdlemk2  34198  cdlemk4  34200  cdlemk8  34204  cdlemkuu  34261  cdlemk53  34323  cdlemk54  34324  cdlemk55a  34325  erngdvlem3  34356  erngdvlem3-rN  34364  tendocnv  34388  tendospcanN  34390  dvhvaddcbv  34456  dvhvaddval  34457  dvhvaddass  34464  dvhvscacbv  34465  dvhvscaval  34466  dvhopvsca  34469  dvhlveclem  34475  dvhopspN  34482  diblss  34537  cdlemn8  34571  dihopelvalcpre  34615  dihmeetlem1N  34657  dihglblem5apreN  34658  dih1dimatlem0  34695  dihjatcclem4  34788