Metamath Proof Explorer

Theorem ralbiim

Description: Split a biconditional and distribute quantifier. Restricted quantifier version of albiim . (Contributed by NM, 3-Jun-2012)

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

Proof

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