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\in V\to A\subseteq \mathrm{wUniCl}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssintub	$$⊢A\subseteq \bigcap \left\{u\in \mathrm{WUni}|A\subseteq u\right\}$$
2		wuncval	$$⊢A\in V\to \mathrm{wUniCl}\left(A\right)=\bigcap \left\{u\in \mathrm{WUni}|A\subseteq u\right\}$$
3	1 2	sseqtrrid	$$⊢A\in V\to A\subseteq \mathrm{wUniCl}\left(A\right)$$