Theorem ralcom4OLD

Description: Obsolete version of ralcom4 as of 31-Oct-2024. (Contributed by NM, 26-Mar-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	ralcom4OLD	$$⊢\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$$