Definition df-slot 15699

Description: Define slot extractor for posets and related structures. Note that the function argument can be any set, although it is meaningful only if it is a member of Poset (df-poset 16769) when used for posets or of Grp (df-grp 17248) when used from groups. (Contributed by Mario Carneiro, 22-Sep-2015.)

Assertion

Ref	Expression
df-slot	⊢ Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥‘𝐴))

Distinct variable group:   𝑥,𝐴

Detailed syntax breakdown of Definition df-slot

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	cslot 15694	. 2 class Slot 𝐴
3		vx	. . 3 setvar 𝑥
4		cvv 3173	. . 3 class V
5	3	cv 1474	. . . 4 class 𝑥
6	1, 5	cfv 5804	. . 3 class (𝑥‘𝐴)
7	3, 4, 6	cmpt 4643	. 2 class (𝑥 ∈ V ↦ (𝑥‘𝐴))
8	2, 7	wceq 1475	1 wff Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥‘𝐴))

This definition is referenced by:  slotfn  15709  strfvnd  15710  ndxid  15716  dfpleOLD  15789