Definition df-elwise 33033

Description: Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 9966), so if A and B are sets of complex numbers, then ( A (elwise ` + ) B ) is the set of numbers of the form ( x + y ) with x e. A and y e. B. The set of odd natural numbers is ( ( { 2 } (elwise ` x. ) NN0 ) (elwise ` + ) { 1 } ), or less formally 2 NN0 + 1. (Contributed by BJ, 22-Dec-2021.)

Assertion

Ref	Expression
df-elwise	|- elwise = ( o e. _V |-> ( x e. _V , y e. _V |-> { z | E. u e. x E. v e. y z = ( u o v ) } ) )

Distinct variable group:   x, o, y, z, u, v

Detailed syntax breakdown of Definition df-elwise

Step	Hyp	Ref	Expression
1		celwise 33032	. 2 class elwise
2		vo	. . 3 setvar o
3		cvv 3200	. . 3 class _V
4		vx	. . . 4 setvar x
5		vy	. . . 4 setvar y
6		vz	. . . . . . . . 9 setvar z
7	6	cv 1482	. . . . . . . 8 class z
8		vu	. . . . . . . . . 10 setvar u
9	8	cv 1482	. . . . . . . . 9 class u
10		vv	. . . . . . . . . 10 setvar v
11	10	cv 1482	. . . . . . . . 9 class v
12	2	cv 1482	. . . . . . . . 9 class o
13	9, 11, 12	co 6650	. . . . . . . 8 class ( u o v )
14	7, 13	wceq 1483	. . . . . . 7 wff z = ( u o v )
15	5	cv 1482	. . . . . . 7 class y
16	14, 10, 15	wrex 2913	. . . . . 6 wff E. v e. y z = ( u o v )
17	4	cv 1482	. . . . . 6 class x
18	16, 8, 17	wrex 2913	. . . . 5 wff E. u e. x E. v e. y z = ( u o v )
19	18, 6	cab 2608	. . . 4 class { z | E. u e. x E. v e. y z = ( u o v ) }
20	4, 5, 3, 3, 19	cmpt2 6652	. . 3 class ( x e. _V , y e. _V |-> { z | E. u e. x E. v e. y z = ( u o v ) } )
21	2, 3, 20	cmpt 4729	. 2 class ( o e. _V |-> ( x e. _V , y e. _V |-> { z | E. u e. x E. v e. y z = ( u o v ) } ) )
22	1, 21	wceq 1483	1 wff elwise = ( o e. _V |-> ( x e. _V , y e. _V |-> { z | E. u e. x E. v e. y z = ( u o v ) } ) )

This definition is referenced by: (None)