Metamath Proof Explorer

Theorem ssrab

Description: Subclass of a restricted class abstraction. (Contributed by NM, 16-Aug-2006)

Ref Expression
Assertion ssrab ⊢ B ⊆ x ∈ A | φ ↔ B ⊆ A ∧ ∀ x ∈ B φ

Proof

Step Hyp Ref Expression
1 df-rab ⊢ x ∈ A | φ = x | x ∈ A ∧ φ
2 1 sseq2i ⊢ B ⊆ x ∈ A | φ ↔ B ⊆ x | x ∈ A ∧ φ
3 ssab ⊢ B ⊆ x | x ∈ A ∧ φ ↔ ∀ x x ∈ B → x ∈ A ∧ φ
4 dfss3 ⊢ B ⊆ A ↔ ∀ x ∈ B x ∈ A
5 4 anbi1i ⊢ B ⊆ A ∧ ∀ x ∈ B φ ↔ ∀ x ∈ B x ∈ A ∧ ∀ x ∈ B φ
6 r19.26 ⊢ ∀ x ∈ B x ∈ A ∧ φ ↔ ∀ x ∈ B x ∈ A ∧ ∀ x ∈ B φ
7 df-ral ⊢ ∀ x ∈ B x ∈ A ∧ φ ↔ ∀ x x ∈ B → x ∈ A ∧ φ
8 5 6 7 3bitr2ri ⊢ ∀ x x ∈ B → x ∈ A ∧ φ ↔ B ⊆ A ∧ ∀ x ∈ B φ
9 2 3 8 3bitri ⊢ B ⊆ x ∈ A | φ ↔ B ⊆ A ∧ ∀ x ∈ B φ