Metamath Proof Explorer

Theorem ralxp3

Description: Restricted for-all over a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Hypothesis ralxp3.1 
|- ( p = <. <. x , y >. , z >. -> ( ph <-> ps ) )
Assertion ralxp3 
|- ( A. p e. ( ( A X. B ) X. C ) ph <-> A. x e. A A. y e. B A. z e. C ps )

Proof

Step Hyp Ref Expression
1 ralxp3.1 
 |-  ( p = <. <. x , y >. , z >. -> ( ph <-> ps ) )
2 nfv 
 |-  F/ x ph
3 nfv 
 |-  F/ y ph
4 nfv 
 |-  F/ z ph
5 nfv 
 |-  F/ p ps
6 2 3 4 5 1 ralxp3f 
 |-  ( A. p e. ( ( A X. B ) X. C ) ph <-> A. x e. A A. y e. B A. z e. C ps )