Metamath Proof Explorer

Theorem ralbi

Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi . (Contributed by NM, 6-Oct-2003) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023)

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

Proof

Step Hyp Ref Expression
1 biimp ⊢ φ ↔ ψ → φ → ψ
2 1 ral2imi ⊢ ∀ x ∈ A φ ↔ ψ → ∀ x ∈ A φ → ∀ x ∈ A ψ
3 biimpr ⊢ φ ↔ ψ → ψ → φ
4 3 ral2imi ⊢ ∀ x ∈ A φ ↔ ψ → ∀ x ∈ A ψ → ∀ x ∈ A φ
5 2 4 impbid ⊢ ∀ x ∈ A φ ↔ ψ → ∀ x ∈ A φ ↔ ∀ x ∈ A ψ