Theorem ralcom4

Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019)

	Ref	Expression
Assertion	ralcom4	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		19.21v	⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) )
2	1	bicomi	⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) ↔ ∀ 𝑦 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
3	2	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
4		alcom	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
5	3 4	bitri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
6		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 𝜑 ) )
7		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
8	7	albii	⊢ ( ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
9	5 6 8	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 𝜑 )