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 ∘ 1st )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccoda coda
1 c2nd 2nd
2 c1st 1st
3 1 2 ccom ( 2nd ∘ 1st )
4 0 3 wceq coda = ( 2nd ∘ 1st )