Metamath Proof Explorer

Theorem coeq1i

Description: Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000)

Ref Expression
Hypothesis coeq1i.1 
|- A = B
Assertion coeq1i 
|- ( A o. C ) = ( B o. C )

Proof

Step Hyp Ref Expression
1 coeq1i.1 
 |-  A = B
2 coeq1 
 |-  ( A = B -> ( A o. C ) = ( B o. C ) )
3 1 2 ax-mp 
 |-  ( A o. C ) = ( B o. C )