Metamath Proof Explorer

Theorem ralcom4OLD

Description: Obsolete version of ralcom4 as of 26-Aug-2023. Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ralcom4OLD ⊢ ∀ x ∈ A ∀ y φ ↔ ∀ y ∀ x ∈ A φ

Proof

Step Hyp Ref Expression
1 ralcom ⊢ ∀ x ∈ A ∀ y ∈ V φ ↔ ∀ y ∈ V ∀ x ∈ A φ
2 ralv ⊢ ∀ y ∈ V φ ↔ ∀ y φ
3 2 ralbii ⊢ ∀ x ∈ A ∀ y ∈ V φ ↔ ∀ x ∈ A ∀ y φ
4 ralv ⊢ ∀ y ∈ V ∀ x ∈ A φ ↔ ∀ y ∀ x ∈ A φ
5 1 3 4 3bitr3i ⊢ ∀ x ∈ A ∀ y φ ↔ ∀ y ∀ x ∈ A φ