Theorem gruelss

Description: A Grothendieck universe is transitive, so each element is a subset of the universe. (Contributed by Mario Carneiro, 9-Jun-2013)

	Ref	Expression
Assertion	gruelss	$$⊢\left(U\in \mathrm{Univ}\wedge A\in U\right)\to A\subseteq U$$

Proof

Step	Hyp	Ref	Expression
1		grutr	$$⊢U\in \mathrm{Univ}\to \mathrm{Tr}U$$
2		trss	$$⊢\mathrm{Tr}U\to \left(A\in U\to A\subseteq U\right)$$
3	2	imp	$$⊢\left(\mathrm{Tr}U\wedge A\in U\right)\to A\subseteq U$$
4	1 3	sylan	$$⊢\left(U\in \mathrm{Univ}\wedge A\in U\right)\to A\subseteq U$$