Metamath Proof Explorer

Definition df-coda

Description: Definition of the codomain extractor for an arrow. (Contributed by FL, 26-Oct-2007) (Revised by Mario Carneiro, 11-Jan-2017)

Ref Expression
Assertion df-coda 
|- codA = ( 2nd o. 1st )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccoda 
 |-  codA
1 c2nd 
 |-  2nd
2 c1st 
 |-  1st
3 1 2 ccom 
 |-  ( 2nd o. 1st )
4 0 3 wceq 
 |-  codA = ( 2nd o. 1st )