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

Theorem coeq2d 5002
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 4998 . 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 4849
This theorem is referenced by:  coeq12d  5004  relcoi1  5365  f1ococnv1  5671  funcoeqres  5673  fcof1o  5993  foeqcnvco  5994  fparlem3  6415  fparlem4  6416  mapen  7238  mapfien  7617  wemapwe  7618  hashfacen  11666  s1co  11765  prdsval  13641  isoval  13953  cofuass  14049  cofurid  14051  fucid  14131  setcinv  14208  catcisolem  14224  curf2ndf  14307  pwsco2mhm  14733  symggrp  15066  efginvrel2  15322  efginvrel1  15323  vrgpinv  15364  frgpuplem  15367  gsumval3  15477  gsumzf1o  15482  psrass1lem  16405  qtophmeo  17810  ustssco  18205  utop2nei  18241  neipcfilu  18287  tngds  18650  elovolmr  19333  ovoliunlem3  19361  uniioombllem2  19436  mpfrcl  19900  evlsval  19901  evl1fval  19908  pf1mpf  19933  pf1ind  19936  hoddi  23454  erdsze2lem2  24851  cvmliftlem10  24942  relexpsucl  25093  relexpadd  25099  dfpo2  25334  cocnv  26325  diophrw  26715  eldioph2  26718  f1omvdco2  27267  psgnunilem1  27292  ltrncoidN  30622  trlcoabs2N  31216  cdlemg47a  31228  cdlemg46  31229  cdlemg47  31230  ltrnco4  31233  tendovalco  31259  tendoplcbv  31269  tendopl  31270  tendoplass  31277  cdlemi2  31313  cdlemk2  31326  cdlemk4  31328  cdlemk8  31332  cdlemkuu  31389  cdlemk53  31451  cdlemk54  31452  cdlemk55a  31453  erngdvlem3  31484  erngdvlem3-rN  31492  tendocnv  31516  tendospcanN  31518  dvhvaddcbv  31584  dvhvaddval  31585  dvhvaddass  31592  dvhvscacbv  31593  dvhvscaval  31594  dvhopvsca  31597  dvhlveclem  31603  dvhopspN  31610  diblss  31665  cdlemn8  31699  dihopelvalcpre  31743  dihmeetlem1N  31785  dihglblem5apreN  31786  dih1dimatlem0  31823  dihjatcclem4  31916
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-in 3295  df-ss 3302  df-br 4181  df-opab 4235  df-co 4854
  Copyright terms: Public domain W3C validator