Metamath Proof Explorer

Theorem rr19.28v

Description: Restricted quantifier version of Theorem 19.28 of Margaris p. 90. We don't need the nonempty class condition of r19.28zv when there is an outer quantifier. (Contributed by NM, 29-Oct-2012)

Ref Expression
Assertion rr19.28v ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ

Proof

Step Hyp Ref Expression
1 simpl ⊢ φ ∧ ψ → φ
2 1 ralimi ⊢ ∀ y ∈ A φ ∧ ψ → ∀ y ∈ A φ
3 biidd ⊢ y = x → φ ↔ φ
4 3 rspcv ⊢ x ∈ A → ∀ y ∈ A φ → φ
5 2 4 syl5 ⊢ x ∈ A → ∀ y ∈ A φ ∧ ψ → φ
6 simpr ⊢ φ ∧ ψ → ψ
7 6 ralimi ⊢ ∀ y ∈ A φ ∧ ψ → ∀ y ∈ A ψ
8 5 7 jca2 ⊢ x ∈ A → ∀ y ∈ A φ ∧ ψ → φ ∧ ∀ y ∈ A ψ
9 8 ralimia ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ → ∀ x ∈ A φ ∧ ∀ y ∈ A ψ
10 r19.28v ⊢ φ ∧ ∀ y ∈ A ψ → ∀ y ∈ A φ ∧ ψ
11 10 ralimi ⊢ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ → ∀ x ∈ A ∀ y ∈ A φ ∧ ψ
12 9 11 impbii ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ