This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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