Theorem 0xp

Description: The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of Monk1 p. 37. (Contributed by NM, 4-Jul-1994)

	Ref	Expression
Assertion	0xp	$$⊢\varnothing \times A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg x\in \varnothing$$
2		simprl	$$⊢\left(z=⟨x,y⟩\wedge \left(x\in \varnothing \wedge y\in A\right)\right)\to x\in \varnothing$$
3	1 2	mto	$$⊢\neg \left(z=⟨x,y⟩\wedge \left(x\in \varnothing \wedge y\in A\right)\right)$$
4	3	nex	$$⊢\neg \exists y\left(z=⟨x,y⟩\wedge \left(x\in \varnothing \wedge y\in A\right)\right)$$
5	4	nex	$$⊢\neg \exists x\exists y\left(z=⟨x,y⟩\wedge \left(x\in \varnothing \wedge y\in A\right)\right)$$
6		elxp	$$⊢z\in \left(\varnothing \times A\right)\leftrightarrow \exists x\exists y\left(z=⟨x,y⟩\wedge \left(x\in \varnothing \wedge y\in A\right)\right)$$
7	5 6	mtbir	$$⊢\neg z\in \left(\varnothing \times A\right)$$
8	7	nel0	$$⊢\varnothing \times A=\varnothing$$