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

Metamath Proof Explorer

Theorem ralcomf

Description: Commutation of restricted universal quantifiers. For a version based on fewer axioms see ralcom . (Contributed by Mario Carneiro, 14-Oct-2016)

Ref Expression
Hypotheses ralcomf.1 ⊢ Ⅎ _ y A
ralcomf.2 ⊢ Ⅎ _ x B
Assertion ralcomf ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ y ∈ B ∀ x ∈ A φ

Proof

Step Hyp Ref Expression
1 ralcomf.1 ⊢ Ⅎ _ y A
2 ralcomf.2 ⊢ Ⅎ _ x B
3 ancomst ⊢ x ∈ A ∧ y ∈ B → φ ↔ y ∈ B ∧ x ∈ A → φ
4 3 2albii ⊢ ∀ x ∀ y x ∈ A ∧ y ∈ B → φ ↔ ∀ x ∀ y y ∈ B ∧ x ∈ A → φ
5 alcom ⊢ ∀ x ∀ y y ∈ B ∧ x ∈ A → φ ↔ ∀ y ∀ x y ∈ B ∧ x ∈ A → φ
6 4 5 bitri ⊢ ∀ x ∀ y x ∈ A ∧ y ∈ B → φ ↔ ∀ y ∀ x y ∈ B ∧ x ∈ A → φ
7 1 r2alf ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ x ∀ y x ∈ A ∧ y ∈ B → φ
8 2 r2alf ⊢ ∀ y ∈ B ∀ x ∈ A φ ↔ ∀ y ∀ x y ∈ B ∧ x ∈ A → φ
9 6 7 8 3bitr4i ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ y ∈ B ∀ x ∈ A φ