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

Metamath Proof Explorer

Theorem ralcomf

Description: Commutation of restricted universal quantifiers. For a version based on fewer axioms see ralcom . (Contributed by Mario Carneiro, 14-Oct-2016)

		Ref	Expression
	Hypotheses	ralcomf.1	⊢ Ⅎ 𝑦 𝐴
		ralcomf.2	⊢ Ⅎ 𝑥 𝐵
	Assertion	ralcomf	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ralcomf.1	⊢ Ⅎ 𝑦 𝐴
2		ralcomf.2	⊢ Ⅎ 𝑥 𝐵
3		ancomst	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 ) )
4	3	2albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 ) )
5		alcom	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 ) )
6	4 5	bitri	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 ) )
7	1	r2alf	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) )
8	2	r2alf	⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 ) )
9	6 7 8	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 )