Metamath Proof Explorer

Theorem ssrabf

Description: Subclass of a restricted class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses ssrabf.1 ⊢ Ⅎ _ x B
ssrabf.2 ⊢ Ⅎ _ x A
Assertion ssrabf ⊢ B ⊆ x ∈ A | φ ↔ B ⊆ A ∧ ∀ x ∈ B φ

Proof

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