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) (Proof shortened by Wolf Lammen, 31-Oct-2024)

	Ref	Expression
Assertion	ralcom4	$$⊢\forall x\in A\forall y\phi \leftrightarrow \forall y\forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		19.21v	$$⊢\forall y\left(x\in A\to \phi \right)\leftrightarrow \left(x\in A\to \forall y\phi \right)$$
2	1	albii	$$⊢\forall x\forall y\left(x\in A\to \phi \right)\leftrightarrow \forall x\left(x\in A\to \forall y\phi \right)$$
3		alcom	$$⊢\forall y\forall x\left(x\in A\to \phi \right)\leftrightarrow \forall x\forall y\left(x\in A\to \phi \right)$$
4		df-ral	$$⊢\forall x\in A\forall y\phi \leftrightarrow \forall x\left(x\in A\to \forall y\phi \right)$$
5	2 3 4	3bitr4ri	$$⊢\forall x\in A\forall y\phi \leftrightarrow \forall y\forall x\left(x\in A\to \phi \right)$$
6		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
7	6	albii	$$⊢\forall y\forall x\in A\phi \leftrightarrow \forall y\forall x\left(x\in A\to \phi \right)$$
8	5 7	bitr4i	$$⊢\forall x\in A\forall y\phi \leftrightarrow \forall y\forall x\in A\phi$$