Metamath Proof Explorer

Theorem 3xpexg

Description: The Cartesian product of three sets is a set. (Contributed by Alexander van der Vekens, 21-Feb-2018)

Ref Expression
Assertion 3xpexg 
|- ( V e. W -> ( ( V X. V ) X. V ) e. _V )

Proof

Step Hyp Ref Expression
1 xpexg 
 |-  ( ( V e. W /\ V e. W ) -> ( V X. V ) e. _V )
2 1 anidms 
 |-  ( V e. W -> ( V X. V ) e. _V )
3 xpexg 
 |-  ( ( ( V X. V ) e. _V /\ V e. W ) -> ( ( V X. V ) X. V ) e. _V )
4 2 3 mpancom 
 |-  ( V e. W -> ( ( V X. V ) X. V ) e. _V )