Metamath Proof Explorer

Theorem ralcom13

Description: Swap first and third restricted universal quantifiers. (Contributed by AV, 3-Dec-2021)

Ref Expression
Assertion ralcom13 ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ z ∈ C ∀ y ∈ B ∀ x ∈ A φ

Proof

Step Hyp Ref Expression
1 ralcom ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ y ∈ B ∀ x ∈ A ∀ z ∈ C φ
2 ralcom ⊢ ∀ x ∈ A ∀ z ∈ C φ ↔ ∀ z ∈ C ∀ x ∈ A φ
3 2 ralbii ⊢ ∀ y ∈ B ∀ x ∈ A ∀ z ∈ C φ ↔ ∀ y ∈ B ∀ z ∈ C ∀ x ∈ A φ
4 ralcom ⊢ ∀ y ∈ B ∀ z ∈ C ∀ x ∈ A φ ↔ ∀ z ∈ C ∀ y ∈ B ∀ x ∈ A φ
5 1 3 4 3bitri ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ z ∈ C ∀ y ∈ B ∀ x ∈ A φ