Metamath Proof Explorer

Theorem wuncid

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

Ref Expression
Assertion wuncid 
|- ( A e. V -> A C_ ( wUniCl ` A ) )

Proof

Step Hyp Ref Expression
1 ssintub 
 |-  A C_ |^| { u e. WUni | A C_ u }
2 wuncval 
 |-  ( A e. V -> ( wUniCl ` A ) = |^| { u e. WUni | A C_ u } )
3 1 2 sseqtrrid 
 |-  ( A e. V -> A C_ ( wUniCl ` A ) )