Theorem ralcomf

Description: Commutation of restricted universal quantifiers. For a version based on fewer axioms see ralcom . (Contributed by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Hypotheses	ralcomf.1	$$⊢\underset{\_}{Ⅎ}yA$$
	ralcomf.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	ralcomf	$$⊢\forall x\in A\forall y\in B\phi \leftrightarrow \forall y\in B\forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		ralcomf.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		ralcomf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		ancomst	$$⊢\left(\left(x\in A\wedge y\in B\right)\to \phi \right)\leftrightarrow \left(\left(y\in B\wedge x\in A\right)\to \phi \right)$$
4	3	2albii	$$⊢\forall x\forall y\left(\left(x\in A\wedge y\in B\right)\to \phi \right)\leftrightarrow \forall x\forall y\left(\left(y\in B\wedge x\in A\right)\to \phi \right)$$
5		alcom	$$⊢\forall x\forall y\left(\left(y\in B\wedge x\in A\right)\to \phi \right)\leftrightarrow \forall y\forall x\left(\left(y\in B\wedge x\in A\right)\to \phi \right)$$
6	4 5	bitri	$$⊢\forall x\forall y\left(\left(x\in A\wedge y\in B\right)\to \phi \right)\leftrightarrow \forall y\forall x\left(\left(y\in B\wedge x\in A\right)\to \phi \right)$$
7	1	r2alf	$$⊢\forall x\in A\forall y\in B\phi \leftrightarrow \forall x\forall y\left(\left(x\in A\wedge y\in B\right)\to \phi \right)$$
8	2	r2alf	$$⊢\forall y\in B\forall x\in A\phi \leftrightarrow \forall y\forall x\left(\left(y\in B\wedge x\in A\right)\to \phi \right)$$
9	6 7 8	3bitr4i	$$⊢\forall x\in A\forall y\in B\phi \leftrightarrow \forall y\in B\forall x\in A\phi$$