Metamath Proof Explorer

Theorem el2xpss

Description: Version of elrel for triple Cartesian products. (Contributed by Scott Fenton, 1-Feb-2025)

Ref Expression
Assertion el2xpss 
|- ( ( A e. R /\ R C_ ( ( B X. C ) X. D ) ) -> E. x E. y E. z A = <. x , y , z >. )

Proof

Step Hyp Ref Expression
1 ssel2 
 |-  ( ( R C_ ( ( B X. C ) X. D ) /\ A e. R ) -> A e. ( ( B X. C ) X. D ) )
2 1 ancoms 
 |-  ( ( A e. R /\ R C_ ( ( B X. C ) X. D ) ) -> A e. ( ( B X. C ) X. D ) )
3 el2xptp 
 |-  ( A e. ( ( B X. C ) X. D ) <-> E. x e. B E. y e. C E. z e. D A = <. x , y , z >. )
4 rexex 
 |-  ( E. z e. D A = <. x , y , z >. -> E. z A = <. x , y , z >. )
5 4 reximi 
 |-  ( E. y e. C E. z e. D A = <. x , y , z >. -> E. y e. C E. z A = <. x , y , z >. )
6 rexex 
 |-  ( E. y e. C E. z A = <. x , y , z >. -> E. y E. z A = <. x , y , z >. )
7 5 6 syl 
 |-  ( E. y e. C E. z e. D A = <. x , y , z >. -> E. y E. z A = <. x , y , z >. )
8 7 reximi 
 |-  ( E. x e. B E. y e. C E. z e. D A = <. x , y , z >. -> E. x e. B E. y E. z A = <. x , y , z >. )
9 rexex 
 |-  ( E. x e. B E. y E. z A = <. x , y , z >. -> E. x E. y E. z A = <. x , y , z >. )
10 8 9 syl 
 |-  ( E. x e. B E. y e. C E. z e. D A = <. x , y , z >. -> E. x E. y E. z A = <. x , y , z >. )
11 3 10 sylbi 
 |-  ( A e. ( ( B X. C ) X. D ) -> E. x E. y E. z A = <. x , y , z >. )
12 2 11 syl 
 |-  ( ( A e. R /\ R C_ ( ( B X. C ) X. D ) ) -> E. x E. y E. z A = <. x , y , z >. )