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 ( ∀ 𝑥𝐴𝑦𝐵 𝜑 ↔ ∀ 𝑦𝐵𝑥𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 ancomst ( ( ( 𝑥𝐴𝑦𝐵 ) → 𝜑 ) ↔ ( ( 𝑦𝐵𝑥𝐴 ) → 𝜑 ) )
2 1 2albii ( ∀ 𝑥𝑦 ( ( 𝑥𝐴𝑦𝐵 ) → 𝜑 ) ↔ ∀ 𝑥𝑦 ( ( 𝑦𝐵𝑥𝐴 ) → 𝜑 ) )
3 alcom ( ∀ 𝑥𝑦 ( ( 𝑦𝐵𝑥𝐴 ) → 𝜑 ) ↔ ∀ 𝑦𝑥 ( ( 𝑦𝐵𝑥𝐴 ) → 𝜑 ) )
4 2 3 bitri ( ∀ 𝑥𝑦 ( ( 𝑥𝐴𝑦𝐵 ) → 𝜑 ) ↔ ∀ 𝑦𝑥 ( ( 𝑦𝐵𝑥𝐴 ) → 𝜑 ) )
5 r2al ( ∀ 𝑥𝐴𝑦𝐵 𝜑 ↔ ∀ 𝑥𝑦 ( ( 𝑥𝐴𝑦𝐵 ) → 𝜑 ) )
6 r2al ( ∀ 𝑦𝐵𝑥𝐴 𝜑 ↔ ∀ 𝑦𝑥 ( ( 𝑦𝐵𝑥𝐴 ) → 𝜑 ) )
7 4 5 6 3bitr4i ( ∀ 𝑥𝐴𝑦𝐵 𝜑 ↔ ∀ 𝑦𝐵𝑥𝐴 𝜑 )