MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  coeq2d Unicode version

Theorem coeq2d 5026
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
StepHypRef Expression
1 coeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 coeq2 5022 . 2  |-  ( A  =  B  ->  ( C  o.  A )  =  ( C  o.  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C  o.  A
)  =  ( C  o.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    o. ccom 4873
This theorem is referenced by:  coeq12d  5028  relcoi1  5389  f1ococnv1  5695  funcoeqres  5697  fcof1o  6017  foeqcnvco  6018  fparlem3  6439  fparlem4  6440  mapen  7262  mapfien  7642  wemapwe  7643  hashfacen  11691  s1co  11790  prdsval  13666  isoval  13978  cofuass  14074  cofurid  14076  fucid  14156  setcinv  14233  catcisolem  14249  curf2ndf  14332  pwsco2mhm  14758  symggrp  15091  efginvrel2  15347  efginvrel1  15348  vrgpinv  15389  frgpuplem  15392  gsumval3  15502  gsumzf1o  15507  psrass1lem  16430  qtophmeo  17837  ustssco  18232  utop2nei  18268  neipcfilu  18314  tngds  18677  elovolmr  19360  ovoliunlem3  19388  uniioombllem2  19463  mpfrcl  19927  evlsval  19928  evl1fval  19935  pf1mpf  19960  pf1ind  19963  hoddi  23481  erdsze2lem2  24878  cvmliftlem10  24969  relexpsucl  25120  relexpadd  25126  dfpo2  25367  cocnv  26364  diophrw  26754  eldioph2  26757  f1omvdco2  27306  psgnunilem1  27331  ltrncoidN  30764  trlcoabs2N  31358  cdlemg47a  31370  cdlemg46  31371  cdlemg47  31372  ltrnco4  31375  tendovalco  31401  tendoplcbv  31411  tendopl  31412  tendoplass  31419  cdlemi2  31455  cdlemk2  31468  cdlemk4  31470  cdlemk8  31474  cdlemkuu  31531  cdlemk53  31593  cdlemk54  31594  cdlemk55a  31595  erngdvlem3  31626  erngdvlem3-rN  31634  tendocnv  31658  tendospcanN  31660  dvhvaddcbv  31726  dvhvaddval  31727  dvhvaddass  31734  dvhvscacbv  31735  dvhvscaval  31736  dvhopvsca  31739  dvhlveclem  31745  dvhopspN  31752  diblss  31807  cdlemn8  31841  dihopelvalcpre  31885  dihmeetlem1N  31927  dihglblem5apreN  31928  dih1dimatlem0  31965  dihjatcclem4  32058
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-in 3319  df-ss 3326  df-br 4205  df-opab 4259  df-co 4878
  Copyright terms: Public domain W3C validator