Metamath Proof Explorer

Theorem gruel

Description: Any element of an element of a Grothendieck universe is also an element of the universe. (Contributed by Mario Carneiro, 9-Jun-2013)

		Ref	Expression
	Assertion	gruel	$⊢ (U \in Univ \land A \in U \land B \in A) \to B \in U$

Step	Hyp	Ref	Expression
1		gruelss	$⊢ (U \in Univ \land A \in U) \to A \subseteq U$
2	1	sseld	$⊢ (U \in Univ \land A \in U) \to (B \in A \to B \in U)$
3	2	3impia	$⊢ (U \in Univ \land A \in U \land B \in A) \to B \in U$