Theorem xpexd

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

	Ref	Expression
Hypotheses	xpexd.1	|- ( ph -> A e. V )
	xpexd.2	|- ( ph -> B e. W )
Assertion	xpexd	|- ( ph -> ( A X. B ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		xpexd.1	|- ( ph -> A e. V )
2		xpexd.2	|- ( ph -> B e. W )
3		xpexg	|- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )
4	1 2 3	syl2anc	|- ( ph -> ( A X. B ) e. _V )