Metamath Proof Explorer

Theorem ralcom

Description: Commutation of restricted universal quantifiers. See ralcom2 for a version without disjoint variable condition on x , y . This theorem should be used in place of ralcom2 since it depends on a smaller set of axioms. (Contributed by NM, 13-Oct-1999) (Revised by Mario Carneiro, 14-Oct-2016)

Ref Expression
Assertion ralcom ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ y ∈ B ∀ x ∈ A φ

Proof

Step Hyp Ref Expression
1 ancomst ⊢ x ∈ A ∧ y ∈ B → φ ↔ y ∈ B ∧ x ∈ A → φ
2 1 2albii ⊢ ∀ x ∀ y x ∈ A ∧ y ∈ B → φ ↔ ∀ x ∀ y y ∈ B ∧ x ∈ A → φ
3 alcom ⊢ ∀ x ∀ y y ∈ B ∧ x ∈ A → φ ↔ ∀ y ∀ x y ∈ B ∧ x ∈ A → φ
4 2 3 bitri ⊢ ∀ x ∀ y x ∈ A ∧ y ∈ B → φ ↔ ∀ y ∀ x y ∈ B ∧ x ∈ A → φ
5 r2al ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ x ∀ y x ∈ A ∧ y ∈ B → φ
6 r2al ⊢ ∀ y ∈ B ∀ x ∈ A φ ↔ ∀ y ∀ x y ∈ B ∧ x ∈ A → φ
7 4 5 6 3bitr4i ⊢ ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ y ∈ B ∀ x ∈ A φ