Metamath Proof Explorer

Theorem r19.26-2

Description: Restricted quantifier version of 19.26-2 . Version of r19.26 with two quantifiers. (Contributed by NM, 10-Aug-2004)

Ref Expression
Assertion r19.26-2 ⊢ ∀ x ∈ A ∀ y ∈ B φ ∧ ψ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ ∀ x ∈ A ∀ y ∈ B ψ

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ∀ y ∈ B φ ∧ ψ ↔ ∀ y ∈ B φ ∧ ∀ y ∈ B ψ
2 1 ralbii ⊢ ∀ x ∈ A ∀ y ∈ B φ ∧ ψ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ ∀ y ∈ B ψ
3 r19.26 ⊢ ∀ x ∈ A ∀ y ∈ B φ ∧ ∀ y ∈ B ψ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ ∀ x ∈ A ∀ y ∈ B ψ
4 2 3 bitri ⊢ ∀ x ∈ A ∀ y ∈ B φ ∧ ψ ↔ ∀ x ∈ A ∀ y ∈ B φ ∧ ∀ x ∈ A ∀ y ∈ B ψ