Metamath Proof Explorer

Theorem ss2ralv

Description: Two quantifications restricted to a subclass. (Contributed by AV, 11-Mar-2023)

Ref Expression
Assertion ss2ralv ⊢ A ⊆ B → ∀ x ∈ B ∀ y ∈ B φ → ∀ x ∈ A ∀ y ∈ A φ

Proof

Step Hyp Ref Expression
1 ssralv ⊢ A ⊆ B → ∀ y ∈ B φ → ∀ y ∈ A φ
2 1 ralimdv ⊢ A ⊆ B → ∀ x ∈ B ∀ y ∈ B φ → ∀ x ∈ B ∀ y ∈ A φ
3 ssralv ⊢ A ⊆ B → ∀ x ∈ B ∀ y ∈ A φ → ∀ x ∈ A ∀ y ∈ A φ
4 2 3 syld ⊢ A ⊆ B → ∀ x ∈ B ∀ y ∈ B φ → ∀ x ∈ A ∀ y ∈ A φ