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	$$⊢\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	bicomi	$$⊢\left(x\in A\to \forall y\phi \right)\leftrightarrow \forall y\left(x\in A\to \phi \right)$$
3	2	albii	$$⊢\forall x\left(x\in A\to \forall y\phi \right)\leftrightarrow \forall x\forall y\left(x\in A\to \phi \right)$$
4		alcom	$$⊢\forall x\forall y\left(x\in A\to \phi \right)\leftrightarrow \forall y\forall x\left(x\in A\to \phi \right)$$
5	3 4	bitri	$$⊢\forall x\left(x\in A\to \forall y\phi \right)\leftrightarrow \forall y\forall x\left(x\in A\to \phi \right)$$
6		df-ral	$$⊢\forall x\in A\forall y\phi \leftrightarrow \forall x\left(x\in A\to \forall y\phi \right)$$
7		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
8	7	albii	$$⊢\forall y\forall x\in A\phi \leftrightarrow \forall y\forall x\left(x\in A\to \phi \right)$$
9	5 6 8	3bitr4i	$$⊢\forall x\in A\forall y\phi \leftrightarrow \forall y\forall x\in A\phi$$