Theorem ralcom4f

Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Revised by Thierry Arnoux, 8-Mar-2017)

	Ref	Expression
Hypothesis	ralcom4f.1	⊢ Ⅎ 𝑦 𝐴
Assertion	ralcom4f	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ralcom4f.1	⊢ Ⅎ 𝑦 𝐴
2		nfcv	⊢ Ⅎ 𝑥 V
3	1 2	ralcomf	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ V 𝜑 ↔ ∀ 𝑦 ∈ V ∀ 𝑥 ∈ 𝐴 𝜑 )
4		ralv	⊢ ( ∀ 𝑦 ∈ V 𝜑 ↔ ∀ 𝑦 𝜑 )
5	4	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ V 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 )
6		ralv	⊢ ( ∀ 𝑦 ∈ V ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 𝜑 )
7	3 5 6	3bitr3i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 𝜑 )