Theorem wunelss

Description: The elements of a weak universe are also subsets of it. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	wununi.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wununi.2	$$⊢\phi \to A\in U$$
Assertion	wunelss	$$⊢\phi \to A\subseteq U$$

Proof

Step	Hyp	Ref	Expression
1		wununi.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		wununi.2	$$⊢\phi \to A\in U$$
3		wuntr	$$⊢U\in \mathrm{WUni}\to \mathrm{Tr}U$$
4	1 3	syl	$$⊢\phi \to \mathrm{Tr}U$$
5		trss	$$⊢\mathrm{Tr}U\to \left(A\in U\to A\subseteq U\right)$$
6	4 2 5	sylc	$$⊢\phi \to A\subseteq U$$