Metamath Proof Explorer


Theorem wuncidm

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

Ref Expression
Assertion wuncidm A V wUniCl wUniCl A = wUniCl A

Proof

Step Hyp Ref Expression
1 wunccl A V wUniCl A WUni
2 ssid wUniCl A wUniCl A
3 wuncss wUniCl A WUni wUniCl A wUniCl A wUniCl wUniCl A wUniCl A
4 1 2 3 sylancl A V wUniCl wUniCl A wUniCl A
5 wuncid wUniCl A WUni wUniCl A wUniCl wUniCl A
6 1 5 syl A V wUniCl A wUniCl wUniCl A
7 4 6 eqssd A V wUniCl wUniCl A = wUniCl A