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

Metamath Proof Explorer

Theorem ssrabdv

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

Ref Expression
Hypotheses ssrabdv.1 ⊢ φ → B ⊆ A
ssrabdv.2 ⊢ φ ∧ x ∈ B → ψ
Assertion ssrabdv ⊢ φ → B ⊆ x ∈ A | ψ

Proof

Step Hyp Ref Expression
1 ssrabdv.1 ⊢ φ → B ⊆ A
2 ssrabdv.2 ⊢ φ ∧ x ∈ B → ψ
3 2 ralrimiva ⊢ φ → ∀ x ∈ B ψ
4 ssrab ⊢ B ⊆ x ∈ A | ψ ↔ B ⊆ A ∧ ∀ x ∈ B ψ
5 1 3 4 sylanbrc ⊢ φ → B ⊆ x ∈ A | ψ