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ψ→φ