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

Metamath Proof Explorer

Theorem ssintrab

Description: Subclass of the intersection of a restricted class abstraction. (Contributed by NM, 30-Jan-2015)

Ref Expression
Assertion ssintrab ⊢ A ⊆ ⋂ x ∈ B | φ ↔ ∀ x ∈ B φ → A ⊆ x

Proof

Step Hyp Ref Expression
1 df-rab ⊢ x ∈ B | φ = x | x ∈ B ∧ φ
2 1 inteqi ⊢ ⋂ x ∈ B | φ = ⋂ x | x ∈ B ∧ φ
3 2 sseq2i ⊢ A ⊆ ⋂ x ∈ B | φ ↔ A ⊆ ⋂ x | x ∈ B ∧ φ
4 impexp ⊢ x ∈ B ∧ φ → A ⊆ x ↔ x ∈ B → φ → A ⊆ x
5 4 albii ⊢ ∀ x x ∈ B ∧ φ → A ⊆ x ↔ ∀ x x ∈ B → φ → A ⊆ x
6 ssintab ⊢ A ⊆ ⋂ x | x ∈ B ∧ φ ↔ ∀ x x ∈ B ∧ φ → A ⊆ x
7 df-ral ⊢ ∀ x ∈ B φ → A ⊆ x ↔ ∀ x x ∈ B → φ → A ⊆ x
8 5 6 7 3bitr4i ⊢ A ⊆ ⋂ x | x ∈ B ∧ φ ↔ ∀ x ∈ B φ → A ⊆ x
9 3 8 bitri ⊢ A ⊆ ⋂ x ∈ B | φ ↔ ∀ x ∈ B φ → A ⊆ x