Theorem coeq2d 5165

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 5161	. 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 1379   o. ccom 5003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-in 3483  df-ss 3490  df-br 4448  df-opab 4506  df-co 5008

This theorem is referenced by:  coeq12d  5167  relcoi1  5536  f1ococnv1  5844  funcoeqres  5846  fcof1oinvd  6185  foeqcnvco  6192  fparlem3  6886  fparlem4  6887  mapen  7682  mapfien  7868  mapfienOLD  8139  wemapwe  8140  wemapweOLD  8141  hashfacen  12470  s1co  12765  prdsval  14713  isoval  15023  cofuass  15119  cofurid  15121  fucid  15201  setcinv  15278  catcisolem  15294  curf2ndf  15377  pwsco2mhm  15824  symggrp  16239  f1omvdco2  16288  psgnunilem1  16333  efginvrel2  16560  efginvrel1  16561  vrgpinv  16602  frgpuplem  16605  gsumval3OLD  16723  gsumval3  16726  gsumzf1o  16732  gsumzf1oOLD  16735  psrass1lem  17840  mpfrcl  17998  evlsval  17999  evls1fval  18167  evl1fval  18175  pf1mpf  18199  pf1ind  18202  ofco2  18760  qtophmeo  20145  ustssco  20544  utop2nei  20580  neipcfilu  20626  tngds  20989  elovolmr  21714  ovoliunlem3  21742  uniioombllem2  21819  hoddi  26682  fcoinver  27230  fcobij  27317  eulerpartlemgv  28063  eulerpartlemn  28071  eulerpart  28072  sseqval  28078  erdsze2lem2  28399  cvmliftlem10  28490  mrsubval  28620  relexpsucl  28806  relexpadd  28812  dfpo2  29037  ftc1anclem8  29950  cocnv  30046  diophrw  30523  eldioph2  30526  ltrncoidN  35141  trlcoabs2N  35735  cdlemg47a  35747  cdlemg46  35748  cdlemg47  35749  ltrnco4  35752  tendovalco  35778  tendoplcbv  35788  tendopl  35789  tendoplass  35796  cdlemi2  35832  cdlemk2  35845  cdlemk4  35847  cdlemk8  35851  cdlemkuu  35908  cdlemk53  35970  cdlemk54  35971  cdlemk55a  35972  erngdvlem3  36003  erngdvlem3-rN  36011  tendocnv  36035  tendospcanN  36037  dvhvaddcbv  36103  dvhvaddval  36104  dvhvaddass  36111  dvhvscacbv  36112  dvhvscaval  36113  dvhopvsca  36116  dvhlveclem  36122  dvhopspN  36129  diblss  36184  cdlemn8  36218  dihopelvalcpre  36262  dihmeetlem1N  36304  dihglblem5apreN  36305  dih1dimatlem0  36342  dihjatcclem4  36435