Metamath Proof Explorer

Theorem r19.26

Description: Restricted quantifier version of 19.26 . (Contributed by NM, 28-Jan-1997) (Proof shortened by Andrew Salmon, 30-May-2011)

Ref Expression
Assertion r19.26 ⊢ ∀ x ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 simpl ⊢ φ ∧ ψ → φ
2 1 ralimi ⊢ ∀ x ∈ A φ ∧ ψ → ∀ x ∈ A φ
3 simpr ⊢ φ ∧ ψ → ψ
4 3 ralimi ⊢ ∀ x ∈ A φ ∧ ψ → ∀ x ∈ A ψ
5 2 4 jca ⊢ ∀ x ∈ A φ ∧ ψ → ∀ x ∈ A φ ∧ ∀ x ∈ A ψ
6 pm3.2 ⊢ φ → ψ → φ ∧ ψ
7 6 ral2imi ⊢ ∀ x ∈ A φ → ∀ x ∈ A ψ → ∀ x ∈ A φ ∧ ψ
8 7 imp ⊢ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ → ∀ x ∈ A φ ∧ ψ
9 5 8 impbii ⊢ ∀ x ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ