This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ W → V × V × V ∈ V

Proof

Step Hyp Ref Expression
1 xpexg ⊢ V ∈ W ∧ V ∈ W → V × V ∈ V
2 1 anidms ⊢ V ∈ W → V × V ∈ V
3 xpexg ⊢ V × V ∈ V ∧ V ∈ W → V × V × V ∈ V
4 2 3 mpancom ⊢ V ∈ W → V × V × V ∈ V