Theorem coeq2d 5023

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 5019	. 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 1369   o. ccom 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-in 3356  df-ss 3363  df-br 4314  df-opab 4372  df-co 4870

This theorem is referenced by:  coeq12d  5025  relcoi1  5387  f1ococnv1  5690  funcoeqres  5692  fcof1o  6018  foeqcnvco  6019  fparlem3  6695  fparlem4  6696  mapen  7496  mapfien  7678  mapfienOLD  7948  wemapwe  7949  wemapweOLD  7950  hashfacen  12228  s1co  12482  prdsval  14414  isoval  14724  cofuass  14820  cofurid  14822  fucid  14902  setcinv  14979  catcisolem  14995  curf2ndf  15078  pwsco2mhm  15520  symggrp  15926  f1omvdco2  15975  psgnunilem1  16020  efginvrel2  16245  efginvrel1  16246  vrgpinv  16287  frgpuplem  16290  gsumval3OLD  16403  gsumval3  16406  gsumzf1o  16412  gsumzf1oOLD  16415  psrass1lem  17469  mpfrcl  17626  evlsval  17627  evls1fval  17776  evl1fval  17784  pf1mpf  17808  pf1ind  17811  ofco2  18354  qtophmeo  19412  ustssco  19811  utop2nei  19847  neipcfilu  19893  tngds  20256  elovolmr  20981  ovoliunlem3  21009  uniioombllem2  21085  hoddi  25416  fcobij  26047  eulerpartlemgv  26778  eulerpartlemn  26786  eulerpart  26787  sseqval  26793  erdsze2lem2  27114  cvmliftlem10  27205  relexpsucl  27356  relexpadd  27362  dfpo2  27587  ftc1anclem8  28500  cocnv  28645  diophrw  29123  eldioph2  29126  ltrncoidN  33868  trlcoabs2N  34462  cdlemg47a  34474  cdlemg46  34475  cdlemg47  34476  ltrnco4  34479  tendovalco  34505  tendoplcbv  34515  tendopl  34516  tendoplass  34523  cdlemi2  34559  cdlemk2  34572  cdlemk4  34574  cdlemk8  34578  cdlemkuu  34635  cdlemk53  34697  cdlemk54  34698  cdlemk55a  34699  erngdvlem3  34730  erngdvlem3-rN  34738  tendocnv  34762  tendospcanN  34764  dvhvaddcbv  34830  dvhvaddval  34831  dvhvaddass  34838  dvhvscacbv  34839  dvhvscaval  34840  dvhopvsca  34843  dvhlveclem  34849  dvhopspN  34856  diblss  34911  cdlemn8  34945  dihopelvalcpre  34989  dihmeetlem1N  35031  dihglblem5apreN  35032  dih1dimatlem0  35069  dihjatcclem4  35162