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