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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssexg | ||
2 | 1 | ancoms | |
3 | wuncval | ||
4 | 2 3 | syl | |
5 | sseq2 | ||
6 | 5 | intminss | |
7 | 4 6 | eqsstrd |