This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem raaan

Description: Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010)

Ref Expression
Hypotheses raaan.1 ⊢ Ⅎ y φ
raaan.2 ⊢ Ⅎ x ψ
Assertion raaan ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ

Proof

Step Hyp Ref Expression
1 raaan.1 ⊢ Ⅎ y φ
2 raaan.2 ⊢ Ⅎ x ψ
3 rzal ⊢ A = ∅ → ∀ x ∈ A ∀ y ∈ A φ ∧ ψ
4 rzal ⊢ A = ∅ → ∀ x ∈ A φ
5 rzal ⊢ A = ∅ → ∀ y ∈ A ψ
6 pm5.1 ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ∧ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ → ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ
7 3 4 5 6 syl12anc ⊢ A = ∅ → ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ
8 1 r19.28z ⊢ A ≠ ∅ → ∀ y ∈ A φ ∧ ψ ↔ φ ∧ ∀ y ∈ A ψ
9 8 ralbidv ⊢ A ≠ ∅ → ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ
10 nfcv ⊢ Ⅎ _ x A
11 10 2 nfralw ⊢ Ⅎ x ∀ y ∈ A ψ
12 11 r19.27z ⊢ A ≠ ∅ → ∀ x ∈ A φ ∧ ∀ y ∈ A ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ
13 9 12 bitrd ⊢ A ≠ ∅ → ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ
14 7 13 pm2.61ine ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ y ∈ A ψ