Theorem raaan

Description: Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010)

	Ref	Expression
Hypotheses	raaan.1	$$⊢Ⅎy\phi$$
	raaan.2	$$⊢Ⅎx\psi$$
Assertion	raaan	$$⊢\forall x\in A\forall y\in A\left(\phi \wedge \psi \right)\leftrightarrow \left(\forall x\in A\phi \wedge \forall y\in A\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		raaan.1	$$⊢Ⅎy\phi$$
2		raaan.2	$$⊢Ⅎx\psi$$
3		rzal	$$⊢A=\varnothing \to \forall x\in A\forall y\in A\left(\phi \wedge \psi \right)$$
4		rzal	$$⊢A=\varnothing \to \forall x\in A\phi$$
5		rzal	$$⊢A=\varnothing \to \forall y\in A\psi$$
6		pm5.1	$$⊢\left(\forall x\in A\forall y\in A\left(\phi \wedge \psi \right)\wedge \left(\forall x\in A\phi \wedge \forall y\in A\psi \right)\right)\to \left(\forall x\in A\forall y\in A\left(\phi \wedge \psi \right)\leftrightarrow \left(\forall x\in A\phi \wedge \forall y\in A\psi \right)\right)$$
7	3 4 5 6	syl12anc	$$⊢A=\varnothing \to \left(\forall x\in A\forall y\in A\left(\phi \wedge \psi \right)\leftrightarrow \left(\forall x\in A\phi \wedge \forall y\in A\psi \right)\right)$$
8	1	r19.28z	$$⊢A\ne \varnothing \to \left(\forall y\in A\left(\phi \wedge \psi \right)\leftrightarrow \left(\phi \wedge \forall y\in A\psi \right)\right)$$
9	8	ralbidv	$$⊢A\ne \varnothing \to \left(\forall x\in A\forall y\in A\left(\phi \wedge \psi \right)\leftrightarrow \forall x\in A\left(\phi \wedge \forall y\in A\psi \right)\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
11	10 2	nfralw	$$⊢Ⅎx\forall y\in A\psi$$
12	11	r19.27z	$$⊢A\ne \varnothing \to \left(\forall x\in A\left(\phi \wedge \forall y\in A\psi \right)\leftrightarrow \left(\forall x\in A\phi \wedge \forall y\in A\psi \right)\right)$$
13	9 12	bitrd	$$⊢A\ne \varnothing \to \left(\forall x\in A\forall y\in A\left(\phi \wedge \psi \right)\leftrightarrow \left(\forall x\in A\phi \wedge \forall y\in A\psi \right)\right)$$
14	7 13	pm2.61ine	$$⊢\forall x\in A\forall y\in A\left(\phi \wedge \psi \right)\leftrightarrow \left(\forall x\in A\phi \wedge \forall y\in A\psi \right)$$