Definition df-intop 41835

Description: Function mapping a set to the class of all internal (binary) operations for this set. (Contributed by AV, 20-Jan-2020.)

Assertion

Ref	Expression
df-intop	|- intOp = ( m e. _V , n e. _V |-> ( n ^m ( m X. m ) ) )

Distinct variable group:   m, n

Detailed syntax breakdown of Definition df-intop

Step	Hyp	Ref	Expression
1		cintop 41832	. 2 class intOp
2		vm	. . 3 setvar m
3		vn	. . 3 setvar n
4		cvv 3200	. . 3 class _V
5	3	cv 1482	. . . 4 class n
6	2	cv 1482	. . . . 5 class m
7	6, 6	cxp 5112	. . . 4 class ( m X. m )
8		cmap 7857	. . . 4 class ^m
9	5, 7, 8	co 6650	. . 3 class ( n ^m ( m X. m ) )
10	2, 3, 4, 4, 9	cmpt2 6652	. 2 class ( m e. _V , n e. _V |-> ( n ^m ( m X. m ) ) )
11	1, 10	wceq 1483	1 wff intOp = ( m e. _V , n e. _V |-> ( n ^m ( m X. m ) ) )

This definition is referenced by:  intopval  41838  intop  41839