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

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

Proof of Theorem coeq2i
StepHypRef Expression
1 coeq1i.1 . 2  |-  A  =  B
2 coeq2 5150 . 2  |-  ( A  =  B  ->  ( C  o.  A )  =  ( C  o.  B ) )
31, 2ax-mp 5 1  |-  ( C  o.  A )  =  ( C  o.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    o. ccom 4992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-in 3468  df-ss 3475  df-br 4440  df-opab 4498  df-co 4997
This theorem is referenced by:  coeq12i  5155  cocnvcnv2  5502  co01  5505  fcoi1  5741  dftpos2  6964  tposco  6978  canthp1  9021  cats1co  12812  isoval  15253  mvdco  16669  evlsval  18383  evl1fval1lem  18561  evl1var  18567  pf1ind  18586  imasdsf1olem  21042  hoico1  26873  hoid1i  26906  pjclem1  27312  pjclem3  27314  pjci  27317  dfpo2  29425  cdlemk45  37070  relexpaddss  38205  trclrelexplem  38229  cotrclrcl  38232  cotrcltrcl  38233  corclrtrcl  38234  cotrclrtrcl  38235  cortrclrcl  38236  cortrcltrcl  38237  cortrclrtrcl  38238
  Copyright terms: Public domain W3C validator