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∈BA⊆x

Proof

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