Theorem gruss

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

	Ref	Expression
Assertion	gruss	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		elpw2g	⊢ ( 𝐴 ∈ 𝑈 → ( 𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
2	1	adantl	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ( 𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
3		grupw	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → 𝒫 𝐴 ∈ 𝑈 )
4		gruelss	⊢ ( ( 𝑈 ∈ Univ ∧ 𝒫 𝐴 ∈ 𝑈 ) → 𝒫 𝐴 ⊆ 𝑈 )
5	3 4	syldan	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → 𝒫 𝐴 ⊆ 𝑈 )
6	5	sseld	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ( 𝐵 ∈ 𝒫 𝐴 → 𝐵 ∈ 𝑈 ) )
7	2 6	sylbird	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ 𝑈 ) )
8	7	3impia	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ 𝑈 )