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

Theorem coeq1d 5037
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 5033 . 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 4885
This theorem is referenced by:  coeq12d  5040  fcof1o  6029  domss2  7269  mapen  7274  mapfien  7656  hashfacen  11708  imasval  13742  cofuass  14091  cofulid  14092  setcinv  14250  catcisolem  14266  catciso  14267  yonedalem3b  14381  gsumvalx  14779  frmdup3  14816  symggrp  15108  gsumval3  15519  gsumzf1o  15524  psrass1lem  16447  coe1add  16662  znval  16821  znle2  16839  dvnfval  19813  evl1sca  19955  evl1var  19957  pf1mpf  19977  pf1ind  19980  hocsubdir  23293  subfacp1lem5  24875  relexpsucr  25135  relexpsucl  25137  relexpcnv  25138  relexpadd  25143  upixp  26445  f1omvdco2  27382  symggen  27402  psgnunilem1  27407  ltrncoidN  30999  trlcoat  31594  trlcone  31599  cdlemg47a  31605  cdlemg47  31607  ltrnco4  31610  tendovalco  31636  tendoplcbv  31646  tendopl  31647  tendoplass  31654  tendo0pl  31662  tendoipl  31668  cdlemk45  31818  cdlemk53b  31827  cdlemk55a  31830  erngdvlem3  31861  erngdvlem3-rN  31869  tendocnv  31893  dvhvaddcbv  31961  dvhvaddval  31962  dvhvaddass  31969  dicvscacl  32063  cdlemn8  32076  dihordlem7b  32087  dihopelvalcpre  32120
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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 4216  df-opab 4270  df-co 4890
  Copyright terms: Public domain W3C validator