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

Theorem coeq2d 4977
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 4973 . 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 1649    o. ccom 4824
This theorem is referenced by:  coeq12d  4979  relcoi1  5340  f1ococnv1  5646  funcoeqres  5648  fcof1o  5967  foeqcnvco  5968  fparlem3  6389  fparlem4  6390  mapen  7209  mapfien  7588  wemapwe  7589  hashfacen  11632  s1co  11731  prdsval  13607  isoval  13919  cofuass  14015  cofurid  14017  fucid  14097  setcinv  14174  catcisolem  14190  curf2ndf  14273  pwsco2mhm  14699  symggrp  15032  efginvrel2  15288  efginvrel1  15289  vrgpinv  15330  frgpuplem  15333  gsumval3  15443  gsumzf1o  15448  psrass1lem  16371  qtophmeo  17772  ustssco  18167  utop2nei  18203  neipcfilu  18249  tngds  18562  elovolmr  19241  ovoliunlem3  19269  uniioombllem2  19344  mpfrcl  19808  evlsval  19809  evl1fval  19816  pf1mpf  19841  pf1ind  19844  hoddi  23343  erdsze2lem2  24671  cvmliftlem10  24762  relexpsucl  24913  relexpadd  24919  dfpo2  25138  cocnv  26120  diophrw  26510  eldioph2  26513  f1omvdco2  27062  psgnunilem1  27087  ltrncoidN  30244  trlcoabs2N  30838  cdlemg47a  30850  cdlemg46  30851  cdlemg47  30852  ltrnco4  30855  tendovalco  30881  tendoplcbv  30891  tendopl  30892  tendoplass  30899  cdlemi2  30935  cdlemk2  30948  cdlemk4  30950  cdlemk8  30954  cdlemkuu  31011  cdlemk53  31073  cdlemk54  31074  cdlemk55a  31075  erngdvlem3  31106  erngdvlem3-rN  31114  tendocnv  31138  tendospcanN  31140  dvhvaddcbv  31206  dvhvaddval  31207  dvhvaddass  31214  dvhvscacbv  31215  dvhvscaval  31216  dvhopvsca  31219  dvhlveclem  31225  dvhopspN  31232  diblss  31287  cdlemn8  31321  dihopelvalcpre  31365  dihmeetlem1N  31407  dihglblem5apreN  31408  dih1dimatlem0  31445  dihjatcclem4  31538
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-in 3272  df-ss 3279  df-br 4156  df-opab 4210  df-co 4829
  Copyright terms: Public domain W3C validator