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

Theorem coeq1d 5036
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
coeq1d  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  C ) )

Proof of Theorem coeq1d
StepHypRef Expression
1 coeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 coeq1 5032 . 2  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    o. ccom 4884
This theorem is referenced by:  coeq12d  5039  fcof1o  6028  domss2  7268  mapen  7273  mapfien  7655  hashfacen  11705  imasval  13739  cofuass  14088  cofulid  14089  setcinv  14247  catcisolem  14263  catciso  14264  yonedalem3b  14378  gsumvalx  14776  frmdup3  14813  symggrp  15105  gsumval3  15516  gsumzf1o  15521  psrass1lem  16444  coe1add  16659  znval  16818  znle2  16836  dvnfval  19810  evl1sca  19952  evl1var  19954  pf1mpf  19974  pf1ind  19977  hocsubdir  23290  subfacp1lem5  24872  relexpsucr  25132  relexpsucl  25134  relexpcnv  25135  relexpadd  25140  upixp  26433  f1omvdco2  27370  symggen  27390  psgnunilem1  27395  ltrncoidN  30987  trlcoat  31582  trlcone  31587  cdlemg47a  31593  cdlemg47  31595  ltrnco4  31598  tendovalco  31624  tendoplcbv  31634  tendopl  31635  tendoplass  31642  tendo0pl  31650  tendoipl  31656  cdlemk45  31806  cdlemk53b  31815  cdlemk55a  31818  erngdvlem3  31849  erngdvlem3-rN  31857  tendocnv  31881  dvhvaddcbv  31949  dvhvaddval  31950  dvhvaddass  31957  dicvscacl  32051  cdlemn8  32064  dihordlem7b  32075  dihopelvalcpre  32108
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-in 3329  df-ss 3336  df-br 4215  df-opab 4269  df-co 4889
  Copyright terms: Public domain W3C validator