Theorem wuncid

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

	Ref	Expression
Assertion	wuncid	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( wUniCl ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ssintub	⊢ 𝐴 ⊆ ∩ { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 }
2		wuncval	⊢ ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ 𝐴 ) = ∩ { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } )
3	1 2	sseqtrrid	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( wUniCl ‘ 𝐴 ) )