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

Theorem coeq1i 5024
Description: Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
Hypothesis
Ref Expression
coeq1i.1  |-  A  =  B
Assertion
Ref Expression
coeq1i  |-  ( A  o.  C )  =  ( B  o.  C
)

Proof of Theorem coeq1i
StepHypRef Expression
1 coeq1i.1 . 2  |-  A  =  B
2 coeq1 5022 . 2  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
31, 2ax-mp 8 1  |-  ( A  o.  C )  =  ( B  o.  C
)
Colors of variables: wff set class
Syntax hints:    = wceq 1652    o. ccom 4874
This theorem is referenced by:  coeq12i  5028  cocnvcnv1  5372  hashgval  11613  imasdsval2  13734  prds1  15712  upxp  17647  uptx  17649  pf1mpf  19964  hoico2  23252  hoid1ri  23285  nmopcoadj2i  23597  pjclem3  23692  erdsze2lem2  24882  pprodcnveq  25720  diblss  31905
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-in 3319  df-ss 3326  df-br 4205  df-opab 4259  df-co 4879
  Copyright terms: Public domain W3C validator