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

Theorem coeq1i 5110
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 5108 . 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 1370    o. ccom 4955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-in 3446  df-ss 3453  df-br 4404  df-opab 4462  df-co 4960
This theorem is referenced by:  coeq12i  5114  cocnvcnv1  5459  hashgval  12227  imasdsval2  14577  prds1  16839  pf1mpf  17921  upxp  19338  uptx  19340  hoico2  25340  hoid1ri  25373  nmopcoadj2i  25685  pjclem3  25780  erdsze2lem2  27259  pprodcnveq  28081  diblss  35178
  Copyright terms: Public domain W3C validator