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 ) |
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 ) |