df-coda - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-coda		Structured version Visualization version GIF version

Definition df-coda 17721

Description: Definition of the codomain extractor for an arrow. (Contributed by FL, 26-Oct-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)

**Assertion**
Ref	Expression
df-coda	⊢ cod_a = (2^nd ∘ 1^st )

**Detailed syntax breakdown of Definition df-coda**
Step	Hyp	Ref	Expression
1		ccoda 17717	. 2 class cod_a
2		c2nd 7816	. . 3 class 2^nd
3		c1st 7815	. . 3 class 1^st
4	2, 3	ccom 5592	. 2 class (2^nd ∘ 1^st )
5	1, 4	wceq 1541	1 wff cod_a = (2^nd ∘ 1^st )

Colors of variables: wff setvar class

This definition is referenced by: homacd 17737 cdaf 17746