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}\circ 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\left(2^{nd}\circ 1^{st}\right)$$
4	0 3	wceq	$$wff{cod}_a=2^{nd}\circ 1^{st}$$