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

Metamath Proof Explorer

Theorem rabssd

Description: Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses rabssd.1 ⊢ Ⅎ x φ
rabssd.2 ⊢ Ⅎ _ x B
rabssd.3 ⊢ φ ∧ x ∈ A ∧ χ → x ∈ B
Assertion rabssd ⊢ φ → x ∈ A | χ ⊆ B

Proof

Step Hyp Ref Expression
1 rabssd.1 ⊢ Ⅎ x φ
2 rabssd.2 ⊢ Ⅎ _ x B
3 rabssd.3 ⊢ φ ∧ x ∈ A ∧ χ → x ∈ B
4 3 3exp ⊢ φ → x ∈ A → χ → x ∈ B
5 1 4 ralrimi ⊢ φ → ∀ x ∈ A χ → x ∈ B
6 2 rabssf ⊢ x ∈ A | χ ⊆ B ↔ ∀ x ∈ A χ → x ∈ B
7 5 6 sylibr ⊢ φ → x ∈ A | χ ⊆ B