Metamath Proof Explorer


Theorem wuncss

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

Ref Expression
Assertion wuncss U WUni A U wUniCl A U

Proof

Step Hyp Ref Expression
1 ssexg A U U WUni A V
2 1 ancoms U WUni A U A V
3 wuncval A V wUniCl A = u WUni | A u
4 2 3 syl U WUni A U wUniCl A = u WUni | A u
5 sseq2 u = U A u A U
6 5 intminss U WUni A U u WUni | A u U
7 4 6 eqsstrd U WUni A U wUniCl A U