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	$$⊢\underset{\_}{Ⅎ}yA$$
Assertion	ralcom4f	$$⊢\forall x\in A\forall y\phi \leftrightarrow \forall y\forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		ralcom4f.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{V}$$
3	1 2	ralcomf	$$⊢\forall x\in A\forall y\in \mathrm{V}\phi \leftrightarrow \forall y\in \mathrm{V}\forall x\in A\phi$$
4		ralv	$$⊢\forall y\in \mathrm{V}\phi \leftrightarrow \forall y\phi$$
5	4	ralbii	$$⊢\forall x\in A\forall y\in \mathrm{V}\phi \leftrightarrow \forall x\in A\forall y\phi$$
6		ralv	$$⊢\forall y\in \mathrm{V}\forall x\in A\phi \leftrightarrow \forall y\forall x\in A\phi$$
7	3 5 6	3bitr3i	$$⊢\forall x\in A\forall y\phi \leftrightarrow \forall y\forall x\in A\phi$$