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 >. -> ( ph <-> ps ) )
Assertion	ralxp	|- ( A. x e. ( A X. B ) ph <-> A. y e. A A. z e. B ps )

Proof

Step	Hyp	Ref	Expression
1		ralxp.1	|- ( x = <. y , z >. -> ( ph <-> ps ) )
2		iunxpconst	|- U_ y e. A ( { y } X. B ) = ( A X. B )
3	2	raleqi	|- ( A. x e. U_ y e. A ( { y } X. B ) ph <-> A. x e. ( A X. B ) ph )
4	1	raliunxp	|- ( A. x e. U_ y e. A ( { y } X. B ) ph <-> A. y e. A A. z e. B ps )
5	3 4	bitr3i	|- ( A. x e. ( A X. B ) ph <-> A. y e. A A. z e. B ps )