Metamath Proof Explorer

Theorem ssint

Description: Subclass of a class intersection. Theorem 5.11(viii) of Monk1 p. 52 and its converse. (Contributed by NM, 14-Oct-1999)

Ref Expression
Assertion ssint ⊢ A ⊆ ⋂ B ↔ ∀ x ∈ B A ⊆ x

Proof

Step Hyp Ref Expression
1 dfss3 ⊢ A ⊆ ⋂ B ↔ ∀ y ∈ A y ∈ ⋂ B
2 vex ⊢ y ∈ V
3 2 elint2 ⊢ y ∈ ⋂ B ↔ ∀ x ∈ B y ∈ x
4 3 ralbii ⊢ ∀ y ∈ A y ∈ ⋂ B ↔ ∀ y ∈ A ∀ x ∈ B y ∈ x
5 ralcom ⊢ ∀ y ∈ A ∀ x ∈ B y ∈ x ↔ ∀ x ∈ B ∀ y ∈ A y ∈ x
6 dfss3 ⊢ A ⊆ x ↔ ∀ y ∈ A y ∈ x
7 6 ralbii ⊢ ∀ x ∈ B A ⊆ x ↔ ∀ x ∈ B ∀ y ∈ A y ∈ x
8 5 7 bitr4i ⊢ ∀ y ∈ A ∀ x ∈ B y ∈ x ↔ ∀ x ∈ B A ⊆ x
9 1 4 8 3bitri ⊢ A ⊆ ⋂ B ↔ ∀ x ∈ B A ⊆ x