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

Theorem coeq2d 4846
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 4842 . 2  |-  ( A  =  B  ->  ( C  o.  A )  =  ( C  o.  B ) )
31, 2syl 15 1  |-  ( ph  ->  ( C  o.  A
)  =  ( C  o.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    o. ccom 4693
This theorem is referenced by:  coeq12d  4848  relcoi1  5201  f1ococnv1  5502  funcoeqres  5504  fcof1o  5803  foeqcnvco  5804  fparlem3  6220  fparlem4  6221  mapen  7025  mapfien  7399  wemapwe  7400  hashfacen  11392  s1co  11488  prdsval  13355  isoval  13667  cofuass  13763  cofurid  13765  fucid  13845  setcinv  13922  catcisolem  13938  curf2ndf  14021  pwsco2mhm  14447  symggrp  14780  efginvrel2  15036  efginvrel1  15037  vrgpinv  15078  frgpuplem  15081  gsumval3  15191  gsumzf1o  15196  psrass1lem  16123  qtophmeo  17508  tngds  18164  elovolmr  18835  ovoliunlem3  18863  uniioombllem2  18938  mpfrcl  19402  evlsval  19403  evl1fval  19410  pf1mpf  19435  pf1ind  19438  hoddi  22570  erdsze2lem2  23735  cvmliftlem10  23825  relexpsucl  24028  relexpadd  24035  dfpo2  24112  valcurfn1  25204  cmpmorass  25966  cmpidmor3  25970  cocnv  26393  diophrw  26838  eldioph2  26841  f1omvdco2  27391  psgnunilem1  27416  ltrncoidN  30317  trlcoabs2N  30911  cdlemg47a  30923  cdlemg46  30924  cdlemg47  30925  ltrnco4  30928  tendovalco  30954  tendoplcbv  30964  tendopl  30965  tendoplass  30972  cdlemi2  31008  cdlemk2  31021  cdlemk4  31023  cdlemk8  31027  cdlemkuu  31084  cdlemk53  31146  cdlemk54  31147  cdlemk55a  31148  erngdvlem3  31179  erngdvlem3-rN  31187  tendocnv  31211  tendospcanN  31213  dvhvaddcbv  31279  dvhvaddval  31280  dvhvaddass  31287  dvhvscacbv  31288  dvhvscaval  31289  dvhopvsca  31292  dvhlveclem  31298  dvhopspN  31305  diblss  31360  cdlemn8  31394  dihopelvalcpre  31438  dihmeetlem1N  31480  dihglblem5apreN  31481  dih1dimatlem0  31518  dihjatcclem4  31611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166  df-br 4024  df-opab 4078  df-co 4698
  Copyright terms: Public domain W3C validator