Theorem r2alf

Description: Double restricted universal quantification. For a version based on fewer axioms see r2al . (Contributed by Mario Carneiro, 14-Oct-2016) Use r2allem . (Revised by Wolf Lammen, 9-Jan-2020)

	Ref	Expression
Hypothesis	r2alf.1	$$⊢\underset{\_}{Ⅎ}yA$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		r2alf.1	$$⊢\underset{\_}{Ⅎ}yA$$
2	1	nfcri	$$⊢Ⅎyx\in A$$
3	2	19.21	$$⊢\forall y\left(x\in A\to \left(y\in B\to \phi \right)\right)\leftrightarrow \left(x\in A\to \forall y\left(y\in B\to \phi \right)\right)$$
4	3	r2allem	$$⊢\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)$$