Metamath Proof Explorer

Theorem ralcom13

Description: Swap first and third restricted universal quantifiers. (Contributed by AV, 3-Dec-2021) (Proof shortened by Wolf Lammen, 2-Jan-2025)

Ref Expression
Assertion ralcom13 ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑧 ∈ 𝐶 ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 ralrot3 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑧 ∈ 𝐶 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 )
2 ralcom ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 )
3 2 ralbii ⊢ ( ∀ 𝑧 ∈ 𝐶 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑧 ∈ 𝐶 ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 )
4 1 3 bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑧 ∈ 𝐶 ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 )