Metamath Proof Explorer

Theorem 2ralbiim

Description: Split a biconditional and distribute two restricted universal quantifiers, analogous to 2albiim and ralbiim . (Contributed by Alexander van der Vekens, 2-Jul-2017)

Ref Expression
Assertion 2ralbiim ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ψ ↔ ∀ x ∈ A ∀ y ∈ B φ → ψ ∧ ∀ x ∈ A ∀ y ∈ B ψ → φ

Proof

Step Hyp Ref Expression
1 ralbiim ⊢ ∀ 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 ψ → φ