This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssintub

Description: Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000)

Ref Expression
Assertion ssintub ⊢ A ⊆ ⋂ x ∈ B | A ⊆ x

Proof

Step Hyp Ref Expression
1 ssint ⊢ A ⊆ ⋂ x ∈ B | A ⊆ x ↔ ∀ y ∈ x ∈ B | A ⊆ x A ⊆ y
2 sseq2 ⊢ x = y → A ⊆ x ↔ A ⊆ y
3 2 elrab ⊢ y ∈ x ∈ B | A ⊆ x ↔ y ∈ B ∧ A ⊆ y
4 3 simprbi ⊢ y ∈ x ∈ B | A ⊆ x → A ⊆ y
5 1 4 mprgbir ⊢ A ⊆ ⋂ x ∈ B | A ⊆ x