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

Theorem coeq2d 5035
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 5031 . 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 4882
This theorem is referenced by:  coeq12d  5037  relcoi1  5398  f1ococnv1  5704  funcoeqres  5706  fcof1o  6026  foeqcnvco  6027  fparlem3  6448  fparlem4  6449  mapen  7271  mapfien  7653  wemapwe  7654  hashfacen  11703  s1co  11802  prdsval  13678  isoval  13990  cofuass  14086  cofurid  14088  fucid  14168  setcinv  14245  catcisolem  14261  curf2ndf  14344  pwsco2mhm  14770  symggrp  15103  efginvrel2  15359  efginvrel1  15360  vrgpinv  15401  frgpuplem  15404  gsumval3  15514  gsumzf1o  15519  psrass1lem  16442  qtophmeo  17849  ustssco  18244  utop2nei  18280  neipcfilu  18326  tngds  18689  elovolmr  19372  ovoliunlem3  19400  uniioombllem2  19475  mpfrcl  19939  evlsval  19940  evl1fval  19947  pf1mpf  19972  pf1ind  19975  hoddi  23493  erdsze2lem2  24890  cvmliftlem10  24981  relexpsucl  25132  relexpadd  25138  dfpo2  25378  ftc1anclem8  26287  cocnv  26427  diophrw  26817  eldioph2  26820  f1omvdco2  27368  psgnunilem1  27393  ltrncoidN  30925  trlcoabs2N  31519  cdlemg47a  31531  cdlemg46  31532  cdlemg47  31533  ltrnco4  31536  tendovalco  31562  tendoplcbv  31572  tendopl  31573  tendoplass  31580  cdlemi2  31616  cdlemk2  31629  cdlemk4  31631  cdlemk8  31635  cdlemkuu  31692  cdlemk53  31754  cdlemk54  31755  cdlemk55a  31756  erngdvlem3  31787  erngdvlem3-rN  31795  tendocnv  31819  tendospcanN  31821  dvhvaddcbv  31887  dvhvaddval  31888  dvhvaddass  31895  dvhvscacbv  31896  dvhvscaval  31897  dvhopvsca  31900  dvhlveclem  31906  dvhopspN  31913  diblss  31968  cdlemn8  32002  dihopelvalcpre  32046  dihmeetlem1N  32088  dihglblem5apreN  32089  dih1dimatlem0  32126  dihjatcclem4  32219
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-in 3327  df-ss 3334  df-br 4213  df-opab 4267  df-co 4887
  Copyright terms: Public domain W3C validator