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

Metamath Proof Explorer

Theorem ssrabdf

Description: Subclass of a restricted class abstraction (deduction form). (Contributed by Glauco Siliprandi, 5-Jan-2025)

Ref Expression
Hypotheses ssrabdf.1 ⊢ Ⅎ _ x A
ssrabdf.2 ⊢ Ⅎ _ x B
ssrabdf.3 ⊢ Ⅎ x φ
ssrabdf.4 ⊢ φ → B ⊆ A
ssrabdf.5 ⊢ φ ∧ x ∈ B → ψ
Assertion ssrabdf ⊢ φ → B ⊆ x ∈ A | ψ

Proof

Step Hyp Ref Expression
1 ssrabdf.1 ⊢ Ⅎ _ x A
2 ssrabdf.2 ⊢ Ⅎ _ x B
3 ssrabdf.3 ⊢ Ⅎ x φ
4 ssrabdf.4 ⊢ φ → B ⊆ A
5 ssrabdf.5 ⊢ φ ∧ x ∈ B → ψ
6 3 5 ralrimia ⊢ φ → ∀ x ∈ B ψ
7 2 1 ssrabf ⊢ B ⊆ x ∈ A | ψ ↔ B ⊆ A ∧ ∀ x ∈ B ψ
8 4 6 7 sylanbrc ⊢ φ → B ⊆ x ∈ A | ψ