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

Theorem coeq1i 4983
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 4981 . 2  |-  ( A  =  B  ->  ( A  o.  C )  =  ( B  o.  C ) )
31, 2ax-mp 5 1  |-  ( A  o.  C )  =  ( B  o.  C
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405    o. ccom 4827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-in 3421  df-ss 3428  df-br 4396  df-opab 4454  df-co 4832
This theorem is referenced by:  coeq12i  4987  cocnvcnv1  5334  hashgval  12455  imasdsval2  15130  prds1  17583  pf1mpf  18708  upxp  20416  uptx  20418  hoico2  27089  hoid1ri  27122  nmopcoadj2i  27434  pjclem3  27529  erdsze2lem2  29501  pprodcnveq  30221  diblss  34190  cortrcltrcl  35719  corclrtrcl  35720  cortrclrcl  35722  cotrclrtrcl  35723  cortrclrtrcl  35724  dvsinax  37076
  Copyright terms: Public domain W3C validator