Definition df-compose 5749

Description: Define the composition function. (Contributed by Scott Fenton, 19-Apr-2021.)

Assertion

Ref	Expression
df-compose	|- Compose = (x e. _V, y e. _V |-> (x o. y))

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-compose

Step	Hyp	Ref	Expression
1		ccompose 5748	. 2 class Compose
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cvv 2860	. . 3 class _V
5	2	cv 1641	. . . 4 class x
6	3	cv 1641	. . . 4 class y
7	5, 6	ccom 4722	. . 3 class (x o. y)
8	2, 3, 4, 4, 7	cmpt2 5654	. 2 class (x e. _V, y e. _V |-> (x o. y))
9	1, 8	wceq 1642	1 wff Compose = (x e. _V, y e. _V |-> (x o. y))

This definition is referenced by:  composevalg  5818  composefn  5819  composeex  5821