Metamath Proof Explorer

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 ⊢ U ∈ Univ ∧ A ∈ U ∧ B ⊆ A → B ∈ U

Proof

Step Hyp Ref Expression
1 elpw2g ⊢ A ∈ U → B ∈ 𝒫 A ↔ B ⊆ A
2 1 adantl ⊢ U ∈ Univ ∧ A ∈ U → B ∈ 𝒫 A ↔ B ⊆ A
3 grupw ⊢ U ∈ Univ ∧ A ∈ U → 𝒫 A ∈ U
4 gruelss ⊢ U ∈ Univ ∧ 𝒫 A ∈ U → 𝒫 A ⊆ U
5 3 4 syldan ⊢ U ∈ Univ ∧ A ∈ U → 𝒫 A ⊆ U
6 5 sseld ⊢ U ∈ Univ ∧ A ∈ U → B ∈ 𝒫 A → B ∈ U
7 2 6 sylbird ⊢ U ∈ Univ ∧ A ∈ U → B ⊆ A → B ∈ U
8 7 3impia ⊢ U ∈ Univ ∧ A ∈ U ∧ B ⊆ A → B ∈ U