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

Metamath Proof Explorer

Theorem xpexd

Description: The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses xpexd.1 ⊢ φ → A ∈ V
xpexd.2 ⊢ φ → B ∈ W
Assertion xpexd ⊢ φ → A × B ∈ V

Proof

Step Hyp Ref Expression
1 xpexd.1 ⊢ φ → A ∈ V
2 xpexd.2 ⊢ φ → B ∈ W
3 xpexg ⊢ A ∈ V ∧ B ∈ W → A × B ∈ V
4 1 2 3 syl2anc ⊢ φ → A × B ∈ V