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

Metamath Proof Explorer

Theorem ss2rabdf

Description: Deduction of restricted abstraction subclass from implication. (Contributed by Glauco Siliprandi, 21-Dec-2024)

Ref Expression
Hypotheses ss2rabdf.1 ⊢ Ⅎ x φ
ss2rabdf.2 ⊢ φ ∧ x ∈ A → ψ → χ
Assertion ss2rabdf ⊢ φ → x ∈ A | ψ ⊆ x ∈ A | χ

Proof

Step Hyp Ref Expression
1 ss2rabdf.1 ⊢ Ⅎ x φ
2 ss2rabdf.2 ⊢ φ ∧ x ∈ A → ψ → χ
3 1 2 ralrimia ⊢ φ → ∀ x ∈ A ψ → χ
4 3 ss2rabd ⊢ φ → x ∈ A | ψ ⊆ x ∈ A | χ