Metamath Proof Explorer

Theorem ralxp3

Description: Restricted for all over a triple Cartesian product. (Contributed by Scott Fenton, 2-Feb-2025)

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

Proof

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