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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ccoda | ||
1 | c2nd | ||
2 | c1st | ||
3 | 1 2 | ccom | |
4 | 0 3 | wceq |