Theorem ralcom3

Description: A commutation law for restricted universal quantifiers that swaps the domains of the restriction. (Contributed by NM, 22-Feb-2004)

	Ref	Expression
Assertion	ralcom3	$$⊢\forall x\in A\left(x\in B\to \phi \right)\leftrightarrow \forall x\in B\left(x\in A\to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		pm2.04	$$⊢\left(x\in A\to \left(x\in B\to \phi \right)\right)\to \left(x\in B\to \left(x\in A\to \phi \right)\right)$$
2	1	ralimi2	$$⊢\forall x\in A\left(x\in B\to \phi \right)\to \forall x\in B\left(x\in A\to \phi \right)$$
3		pm2.04	$$⊢\left(x\in B\to \left(x\in A\to \phi \right)\right)\to \left(x\in A\to \left(x\in B\to \phi \right)\right)$$
4	3	ralimi2	$$⊢\forall x\in B\left(x\in A\to \phi \right)\to \forall x\in A\left(x\in B\to \phi \right)$$
5	2 4	impbii	$$⊢\forall x\in A\left(x\in B\to \phi \right)\leftrightarrow \forall x\in B\left(x\in A\to \phi \right)$$