Metamath Proof Explorer

Theorem ralcom4f

Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Revised by Thierry Arnoux, 8-Mar-2017)

Ref Expression
Hypothesis ralcom4f.1 ⊢ Ⅎ _ y A
Assertion ralcom4f ⊢ ∀ x ∈ A ∀ y φ ↔ ∀ y ∀ x ∈ A φ

Proof

Step Hyp Ref Expression
1 ralcom4f.1 ⊢ Ⅎ _ y A
2 nfcv ⊢ Ⅎ _ x V
3 1 2 ralcomf ⊢ ∀ x ∈ A ∀ y ∈ V φ ↔ ∀ y ∈ V ∀ x ∈ A φ
4 ralv ⊢ ∀ y ∈ V φ ↔ ∀ y φ
5 4 ralbii ⊢ ∀ x ∈ A ∀ y ∈ V φ ↔ ∀ x ∈ A ∀ y φ
6 ralv ⊢ ∀ y ∈ V ∀ x ∈ A φ ↔ ∀ y ∀ x ∈ A φ
7 3 5 6 3bitr3i ⊢ ∀ x ∈ A ∀ y φ ↔ ∀ y ∀ x ∈ A φ