Metamath Proof Explorer


Theorem wunccl

Description: The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion wunccl A V wUniCl A WUni

Proof

Step Hyp Ref Expression
1 wuncval A V wUniCl A = u WUni | A u
2 ssrab2 u WUni | A u WUni
3 wunex A V u WUni A u
4 rabn0 u WUni | A u u WUni A u
5 3 4 sylibr A V u WUni | A u
6 intwun u WUni | A u WUni u WUni | A u u WUni | A u WUni
7 2 5 6 sylancr A V u WUni | A u WUni
8 1 7 eqeltrd A V wUniCl A WUni