Metamath Proof Explorer


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 )