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	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		gruelss	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ⊆ 𝑈 )
2	1	sseld	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ( 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝑈 ) )
3	2	3impia	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ 𝑈 )