Metamath Proof Explorer

Theorem coeq2i

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

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

Proof

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