Theorem ralxp

Description: Universal quantification restricted to a Cartesian product is equivalent to a double restricted quantification. The hypothesis specifies an implicit substitution. (Contributed by NM, 7-Feb-2004) (Revised by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypothesis	ralxp.1	$$⊢x=⟨y,z⟩\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ralxp	$$⊢\forall x\in \left(A\times B\right)\phi \leftrightarrow \forall y\in A\forall z\in B\psi$$

Proof

Step	Hyp	Ref	Expression
1		ralxp.1	$$⊢x=⟨y,z⟩\to \left(\phi \leftrightarrow \psi \right)$$
2		iunxpconst	$$⊢\bigcup _{y\in A}\left(\left\{y\right\}\times B\right)=A\times B$$
3	2	raleqi	$$⊢\forall x\in \bigcup _{y\in A}\left(\left\{y\right\}\times B\right)\phi \leftrightarrow \forall x\in \left(A\times B\right)\phi$$
4	1	raliunxp	$$⊢\forall x\in \bigcup _{y\in A}\left(\left\{y\right\}\times B\right)\phi \leftrightarrow \forall y\in A\forall z\in B\psi$$
5	3 4	bitr3i	$$⊢\forall x\in \left(A\times B\right)\phi \leftrightarrow \forall y\in A\forall z\in B\psi$$