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 cod a = 2 nd 1 st

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccoda class cod a
1 c2nd class 2 nd
2 c1st class 1 st
3 1 2 ccom class 2 nd 1 st
4 0 3 wceq wff cod a = 2 nd 1 st