Definition df-wunc 9525

Description: A function that maps a set x to the smallest weak universe that contains the elements of the set. (Contributed by Mario Carneiro, 2-Jan-2017.)

Assertion

Ref	Expression
df-wunc	|- wUniCl = ( x e. _V |-> |^| { u e. WUni | x C_ u } )

Distinct variable group:   x, u

Detailed syntax breakdown of Definition df-wunc

Step	Hyp	Ref	Expression
1		cwunm 9523	. 2 class wUniCl
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . . 6 class x
5		vu	. . . . . . 7 setvar u
6	5	cv 1482	. . . . . 6 class u
7	4, 6	wss 3574	. . . . 5 wff x C_ u
8		cwun 9522	. . . . 5 class WUni
9	7, 5, 8	crab 2916	. . . 4 class { u e. WUni | x C_ u }
10	9	cint 4475	. . 3 class |^| { u e. WUni | x C_ u }
11	2, 3, 10	cmpt 4729	. 2 class ( x e. _V |-> |^| { u e. WUni | x C_ u } )
12	1, 11	wceq 1483	1 wff wUniCl = ( x e. _V |-> |^| { u e. WUni | x C_ u } )

This definition is referenced by:  wuncval  9564