Metamath Proof Explorer

Theorem elxpxp

Description: Membership in a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Assertion elxpxp 
|- ( A e. ( ( B X. C ) X. D ) <-> E. x e. B E. y e. C E. z e. D A = <. <. x , y >. , z >. )

Proof

Step Hyp Ref Expression
1 elxp2 
 |-  ( A e. ( ( B X. C ) X. D ) <-> E. p e. ( B X. C ) E. z e. D A = <. p , z >. )
2 opeq1 
 |-  ( p = <. x , y >. -> <. p , z >. = <. <. x , y >. , z >. )
3 2 eqeq2d 
 |-  ( p = <. x , y >. -> ( A = <. p , z >. <-> A = <. <. x , y >. , z >. ) )
4 3 rexbidv 
 |-  ( p = <. x , y >. -> ( E. z e. D A = <. p , z >. <-> E. z e. D A = <. <. x , y >. , z >. ) )
5 4 rexxp 
 |-  ( E. p e. ( B X. C ) E. z e. D A = <. p , z >. <-> E. x e. B E. y e. C E. z e. D A = <. <. x , y >. , z >. )
6 1 5 bitri 
 |-  ( A e. ( ( B X. C ) X. D ) <-> E. x e. B E. y e. C E. z e. D A = <. <. x , y >. , z >. )