Definition df-compose 5748

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 5747	. 2 class Compose
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cvv 2859	. . 3 class _V
5	2	cv 1641	. . . 4 class x
6	3	cv 1641	. . . 4 class y
7	5, 6	ccom 4721	. . 3 class (x o. y)
8	2, 3, 4, 4, 7	cmpt2 5653	. 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  5817  composefn  5818  composeex  5820