Definition df-bj-sethom 33078

Description: Define the set of functions (morphisms of sets) between two sets. Same as df-map 7859 with arguments swapped. TODO: prove the same staple lemmas as for ^m.

Remark: one may define -Set-> = ( x e. ( 1st Struct ) , y e. ( 1st Struct ) |-> { f | f : ( Base x ) --> ( Base y ) } ) so that for morphisms between other structures, one could write ... { f e. ( x -Set-> y ) |...

(Contributed by BJ, 11-Apr-2020.)

Assertion

Ref	Expression
df-bj-sethom	|- -Set-> = ( x e. _V , y e. _V |-> { f | f : x --> y } )

Distinct variable group:   x, f, y

Detailed syntax breakdown of Definition df-bj-sethom

Step	Hyp	Ref	Expression
1		csethom 33075	. 2 class -Set->
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . . 5 class x
6	3	cv 1482	. . . . 5 class y
7		vf	. . . . . 6 setvar f
8	7	cv 1482	. . . . 5 class f
9	5, 6, 8	wf 5884	. . . 4 wff f : x --> y
10	9, 7	cab 2608	. . 3 class { f | f : x --> y }
11	2, 3, 4, 4, 10	cmpt2 6652	. 2 class ( x e. _V , y e. _V |-> { f | f : x --> y } )
12	1, 11	wceq 1483	1 wff -Set-> = ( x e. _V , y e. _V |-> { f | f : x --> y } )

This definition is referenced by: (None)