Definition df-tskm 9660

Description: A function that maps a set x to the smallest Tarski class that contains the set. (Contributed by FL, 30-Dec-2010.)

Assertion

Ref	Expression
df-tskm	|- tarskiMap = ( x e. _V |-> |^| { y e. Tarski | x e. y } )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-tskm

Step	Hyp	Ref	Expression
1		ctskm 9659	. 2 class tarskiMap
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		vy	. . . . . 6 setvar y
5	2, 4	wel 1991	. . . . 5 wff x e. y
6		ctsk 9570	. . . . 5 class Tarski
7	5, 4, 6	crab 2916	. . . 4 class { y e. Tarski | x e. y }
8	7	cint 4475	. . 3 class |^| { y e. Tarski | x e. y }
9	2, 3, 8	cmpt 4729	. 2 class ( x e. _V |-> |^| { y e. Tarski | x e. y } )
10	1, 9	wceq 1483	1 wff tarskiMap = ( x e. _V |-> |^| { y e. Tarski | x e. y } )

This definition is referenced by:  tskmval  9661