Theorem r2al

Description: Double restricted universal quantification. (Contributed by NM, 19-Nov-1995) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Jan-2020)

	Ref	Expression
Assertion	r2al	$$⊢\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		19.21v	$$⊢\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)$$
2	1	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)$$