Metamath Proof Explorer

Theorem raaanv

Description: Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997)

Ref Expression
Assertion raaanv ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ

Proof

Step Hyp Ref Expression
1 rzal ⊢ A = ∅ → ∀ x ∈ A ∀ y ∈ A φ ∧ ψ
2 rzal ⊢ A = ∅ → ∀ x ∈ A φ
3 rzal ⊢ A = ∅ → ∀ y ∈ A ψ
4 pm5.1 ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ∧ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ → ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ
5 1 2 3 4 syl12anc ⊢ A = ∅ → ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ
6 r19.28zv ⊢ A ≠ ∅ → ∀ y ∈ A φ ∧ ψ ↔ φ ∧ ∀ y ∈ A ψ
7 6 ralbidv ⊢ A ≠ ∅ → ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ
8 r19.27zv ⊢ A ≠ ∅ → ∀ x ∈ A φ ∧ ∀ y ∈ A ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ
9 7 8 bitrd ⊢ A ≠ ∅ → ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ
10 5 9 pm2.61ine ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ