Metamath Proof Explorer


Definition df-wunc

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)

Ref Expression
Assertion df-wunc wUniCl = x V u WUni | x u

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwunm class wUniCl
1 vx setvar x
2 cvv class V
3 vu setvar u
4 cwun class WUni
5 1 cv setvar x
6 3 cv setvar u
7 5 6 wss wff x u
8 7 3 4 crab class u WUni | x u
9 8 cint class u WUni | x u
10 1 2 9 cmpt class x V u WUni | x u
11 0 10 wceq wff wUniCl = x V u WUni | x u