Metamath Proof Explorer

Theorem el2xptp

Description: A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018)

Ref Expression
Assertion el2xptp 
|- ( 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 df-ot 
 |-  <. x , y , z >. = <. <. x , y >. , z >.
7 6 eqcomi 
 |-  <. <. x , y >. , z >. = <. x , y , z >.
8 7 eqeq2i 
 |-  ( A = <. <. x , y >. , z >. <-> A = <. x , y , z >. )
9 8 rexbii 
 |-  ( E. z e. D A = <. <. x , y >. , z >. <-> E. z e. D A = <. x , y , z >. )
10 9 rexbii 
 |-  ( E. y e. C E. z e. D A = <. <. x , y >. , z >. <-> E. y e. C E. z e. D A = <. x , y , z >. )
11 10 rexbii 
 |-  ( E. x e. B E. y e. C E. z e. D A = <. <. x , y >. , z >. <-> E. x e. B E. y e. C E. z e. D A = <. x , y , z >. )
12 1 5 11 3bitri 
 |-  ( A e. ( ( B X. C ) X. D ) <-> E. x e. B E. y e. C E. z e. D A = <. x , y , z >. )